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

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ (B * A).rank = B.rank

Tactic:
by
  nontriviality R
  refine le_antisymm (rank_mul_le_left B A) ?_
  have key : (B * A) * A.adjugate = A.det • B := by
    rw [Matrix.mul_assoc, Matrix.mul_adjugate, Matrix.mul_smul, Matrix.mul_one]
  calc B.rank = (A.det • B).rank := (rank_smul_of_mem_nonZeroDivisors B hA).symm
    _ = ((B * A) * A.adjugate).rank := by rw [key]
    _ ≤ (B * A).rank := rank_mul_le_left _ _

Goal state after:
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} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
⊢ (constantCoeff ψ).natDegree ≤ finrank K L - r

Tactic:
rw [constantCoeff_apply]

Goal state after:
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} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
⊢ (ψ.coeff 0).natDegree ≤ finrank K L - r
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ finrank R ↥(span R (range M.row)) = Fintype.card m

Tactic:
linearIndependent_iff_card_eq_finrank_span.mp h,

Goal state after:
m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M.row
⊢ finrank R ↥(span R (range M.row)) = Set.finrank R (range M.row)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case h
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
α : K
hα : α ∈ s
v : ↥U := ⋯
z : L
z' : Q := ⋯
n : ℕ
hn : ((ad K L) ↑v ^ n) z = 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0

Tactic:
apply_fun LieSubmodule.Quotient.mk' E at hn

Goal state after:
case h
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} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
z' : Q := (LieSubmodule.Quotient.mk' E) z
n : ℕ
hn : (LieSubmodule.Quotient.mk' E) (((ad K L) ↑v ^ n) z) = (LieSubmodule.Quotient.mk' E) 0
⊢ ((toEnd K (↥U) Q) v ^ n) z' = 0
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = ⁅x✝², x✝¹⁆ x✝ + x✝¹ (x✝² x✝)

Tactic:
rw [commutator_apply]

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
x✝² x✝¹ : Derivation R A A
x✝ : A
⊢ x✝² (x✝¹ x✝) = x✝² (x✝¹ x✝) - x✝¹ (x✝² x✝) + x✝¹ (x✝² x✝)
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨single m b + y, hmby⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby⟩

Tactic:
have : Disjoint (Finsupp.single m b).support y.coeff.support := by
      simpa only [Finsupp.support_single _ hb, Finset.disjoint_singleton_left]

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) i
this : Disjoint (Finsupp.single m b).support y.coeff.support
⊢ (decomposeAux f) ↑⟨single m b + y, hmby⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby⟩
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: case hadd.hadd.e_a
ι : 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
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ k • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) +
      ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a, φ k • (of (fun x ↦ ↥(ℒ x)) k) b⁆ j) -
      ↑((φ i • -⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆) j)

Tactic:
sub_eq_add_neg,

Goal state after:
case hadd.hadd.e_a
ι : 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
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ k • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) +
      ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a, φ k • (of (fun x ↦ ↥(ℒ x)) k) b⁆ j) +
      -↑((φ i • -⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆) j)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).support = s.toFinset

Tactic:
by
  obtain ⟨s⟩ := s
  refine support_formPerm_of_nodup s h ?_
  rintro _ rfl
  simpa [Nat.succ_le_succ_iff] using length_nontrivial hn

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∉ p.support
⊢ (p.toList x).Nodup

Tactic:
← toList_eq_nil_iff

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : p.toList x = []
⊢ (p.toList x).Nodup
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ f.toList y = []

Tactic:
toList_eq_nil_iff

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ y ∉ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ x ∈ s.toFinset

Tactic:
simpa using hx

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

Goal state before:
pp: case intro.refine_2.mk.refine_1
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
hx : l.length < 2
⊢ l.length ≤ 1

Tactic:
exact Nat.le_of_lt_succ hx

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

Goal state before:
pp: case intro.refine_2.mk.refine_2
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
val✝ : Fintype α
x : α
y✝ : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α)) l) hn).SameCycle x y
⊢ x ∈ l.formPerm.support

Tactic:
simpa using hx

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

Goal state before:
pp: n p : ℕ
i : Fin n
⊢ S (p + 1) i = (Finset.Ioi i).biUnion fun k ↦ Finset.image (Fin.cons k) (S p k)

Tactic:
ext α

Goal state after:
n p : ℕ
i : Fin n
α : Fin (p + 1) → Fin n
⊢ α ∈ S (p + 1) i ↔ α ∈ (Finset.Ioi i).biUnion fun k ↦ Finset.image (Fin.cons k) (S p k)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| i + 1

Tactic:
← Finset.card_fin (i + 1)

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| Finset.univ.card
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
exact second_of_chain_is_irreducible hn h₁ (@h₂) hq

Goal state after:
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
⊢ coeSubmodule P ⊤ = 1

Tactic:
coeSubmodule_top

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ 1 = 1
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
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ (↑↑I).FG

Tactic:
exact FractionalIdeal.fg_of_isUnit (R := R) I h

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

Goal state before:
pp: case pos
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
hI : I = 0
⊢ I * (1 / I) ≤ 1

pp: case neg
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
hI : ¬I = 0
⊢ I * (1 / I) ≤ 1

Tactic:
· rw [hI, div_zero, mul_zero]
    exact zero_le 1

Goal state after:
case neg
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
hI : ¬I = 0
⊢ I * (1 / I) ≤ 1
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
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I : ∀ β_lin ∈ q, β_lin ≠ 0 → genWeightSpace L ⇑β_lin ≤ I
h_plus_contain : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ≤ I
this : -Weight.toLinear K (↥H) L α = -1 • Weight.toLinear K (↥H) L α
⊢ Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ∈ q

Tactic:
sub_eq_add_neg,

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
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
h_h_containment : ⁅x_χ, ↑y⁆ ∈ genWeightSpace L ⇑χ
h_bracket_decomp :
  ⁅x_χ, m_α⁆ ∈
    genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ⊔
        genWeightSpace L (⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α)) ⊔
      genWeightSpace L ⇑χ
I : LieSubmodule K (↥H) L := ⨆ β, sl2SubmoduleOfRoot ⋯
genWeightSpace_le_I : ∀ β_lin ∈ q, β_lin ≠ 0 → genWeightSpace L ⇑β_lin ≤ I
h_plus_contain : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) ≤ I
this : -Weight.toLinear K (↥H) L α = -1 • Weight.toLinear K (↥H) L α
⊢ Weight.toLinear K (↥H) L χ + -Weight.toLinear K (↥H) L α ∈ q
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
· rw [mem_canonicalEquiv_apply]
    obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h
    use z • x
    use (mem_spanSingleton _).mpr ⟨z, rfl⟩
    simp [IsLocalization.map_smul]

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

Goal state before:
pp: R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : Ideal.span {a} = 0
⊢ False

Tactic:
rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h

Goal state after:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : a = 0
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J ∣ I ⊓ J

Tactic:
rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : Module R N
⊢ index 0 = ↑(finrank R M) - ↑(finrank R N)

Tactic:
rw [index_eq_finrank_sub, ker_zero, range_zero]
  simpa using (Submodule.quotEquivOfEqBot _ rfl).finrank_eq

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
x✝ : ↥⋯.toFinset
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, l (b a) = x

Tactic:
simpa using hx

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✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ (idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩

Tactic:
exact (idealFactorsEquivOfQuotEquiv f).le_iff_le

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
hJ0 : J = 0
⊢ J * K ∣ I

Tactic:
simpa only [hJ0, zero_mul] using hJ

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ IsUnit ((algebraMap R (Module.End R N)) (↑u * r))

pp: case refine_2
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ ∀ (x : N), ∃ n y, (↑u * r) ^ n • x = f y

pp: case refine_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ ∀ (x y : M), f x = f y → ∃ n, (↑u * r) ^ n • x = (↑u * r) ^ n • y

Tactic:
· simp [IsUnit.mul, isUnit_algebraMap f r, u.isUnit.map _]

Goal state after:
case refine_2
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ ∀ (x : N), ∃ n y, (↑u * r) ^ n • x = f y

case refine_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
f : M →ₗ[R] N
r : R
inst✝ : IsLocalizedModule.Away r f
u : Rˣ
⊢ ∀ (x y : M), f x = f y → ∃ n, (↑u * r) ^ n • x = (↑u * r) ^ n • y
Module: Mathlib.Algebra.Module.FinitePresentation

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

Tactic:
top_inf_eq,

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