mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
⊢ (B.restrict p) ⟨z, hz⟩ = 0

Tactic:
· ext ⟨x, hx⟩
    simpa using LinearMap.congr_fun h x

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
⊢ IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)

Tactic:
refine ⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩

Goal state after:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ Codisjoint W (B.orthogonal W)
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x y : L
⊢ Commute ((toEnd R L M) x) ((toEnd R L M) y)

Tactic:
by
      rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
x : L
hx : x ∈ I
⊢ x ∈ s.sup id

Tactic:
exact hI.le hx

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst = v
hx2 : ↑x.snd = count v m
⊢ consEquiv x = none

Tactic:
by simp [consEquiv, hx, hx2]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (MvPolynomial (Vars k) k ⧸ maxIdeal k)) ↑f).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Tactic:
rw [← Ideal.Quotient.mk_comp_algebraMap, ← map_map, ← Polynomial.map_prod, ← sub_eq_zero,
    ← coeff_sub, ← Polynomial.map_sub, ← subProdXSubC, coeff_map, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (subProdXSubC f).coeff n✝ ∈ maxIdeal k
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : IsKilling R L
inst✝² : IsNoetherian R L
inst✝¹ : IsArtinian R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥

Tactic:
by
  have h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R H L) :=
    (LieModule.isCompl_genWeightSpace_zero_posFittingComp R H L).codisjoint
  replace h : Codisjoint (H : Submodule R L) (LieModule.posFittingComp R H L : Submodule R L) := by
    rwa [codisjoint_iff, ← LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule,
      LieSubmodule.top_toSubmodule, rootSpace_zero_eq R L H, LieSubalgebra.coe_toLieSubmodule,
      ← codisjoint_iff] at h
  suffices this : ∀ m₀ ∈ H, ∀ m₁ ∈ LieModule.posFittingComp R H L, killingForm R L m₀ m₁ = 0 by
    simp [LinearMap.BilinForm.ker_restrict_eq_of_codisjoint h this]
  intro m₀ h₀ m₁ h₁
  exact killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting R L H (le_zeroRootSubalgebra R L H h₀) h₁

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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆
m₀ m₁ : M
hm₀ : m₀ ∈ genWeightSpace M 0
hm₁ : m₁ ∈ posFittingComp R L M
x : L
k : ℕ
ih : ∀ (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
⊢ ∀ (m n : M), (B m) ((φ x ^ (k + 1)) n) = (-1) ^ (k + 1) • (B ((φ x ^ (k + 1)) m)) n

Tactic:
intro m n
    replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
    have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ (-1 : R), smul_eq_mul]
    conv_lhs => rw [pow_succ, Module.End.mul_eq_comp, LinearMap.comp_apply, ih, hB,
      ← (φ x).comp_apply, ← Module.End.mul_eq_comp, ← pow_succ', ← smul_assoc, this]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
⊢ (Ne on fun i ↦ (g i • ↑S i).degree) x y

Tactic:
have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i ↦ (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
⊢ (Ne on fun i ↦ (g i • ↑S i).degree) x y
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ (Weight.toLinear K (↥H) L α) (coroot α) = 2

Tactic:
simpa [coroot] using inv_mul_cancel₀ (root_apply_cartanEquivDual_symm_ne_zero hα)

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ ((reflection hg * reflection hf) ^ m) z =
    z +
        (Polynomial.eval t (S R ((-↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((-↑m - 1) / 2)) + Polynomial.eval t (S R ((-↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((-↑m - 1) / 2)) *
          (Polynomial.eval t (S R (-↑m / 2)) + Polynomial.eval t (S R ((-↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
reflection_mul_reflection_pow_apply hg hf m z t ht',

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((f y * g z - f z) • x - g z • y) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((g x * f z - g z) • y - f z • x) =
    z +
        (Polynomial.eval t (S R ((-↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((-↑m - 1) / 2)) + Polynomial.eval t (S R ((-↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((-↑m - 1) / 2)) *
          (Polynomial.eval t (S R (-↑m / 2)) + Polynomial.eval t (S R ((-↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
χ : Weight K (↥H) L
hχ : χ ∈ LieSubalgebra.root
⊢ χ.IsNonZero

Tactic:
simpa [LieSubalgebra.root] using hχ

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.root i = -P.root j
⊢ P.root i = P.root ((P.reflectionPerm j) j)

Tactic:
root_reflectionPerm,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.root i = -P.root j
⊢ P.root i = (P.reflection j) (P.root j)
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x : N
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

Tactic:
replace h : P.root' j = t • P.root' i := by ext; simp [h, root']

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree N
i j : ι
t : R
hij : t * P.pairing i j = 2
x : N
h : P.root' j = t • P.root' i
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflectionPerm i = P.reflectionPerm j
⊢ P.reflection i = P.reflection j

Tactic:
suffices ⇑(P.reflection i) = ⇑(P.reflection j) from DFunLike.coe_injective this

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h2 : IsSMulRegular M 2
h : P.reflectionPerm i = P.reflectionPerm j
⊢ ⇑(P.reflection i) = ⇑(P.reflection j)
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ (algebraMap S R) (((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) m) n) = (algebraMap S R) (g n)

Tactic:
change Algebra.linearMap S R _ = _

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h : ∀ (g : Dual S N'), ∃ m, ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
g : Dual S N'
m : M'
hm : ↑S (p.toPerfPair (i m)) ∘ₗ j = Algebra.linearMap S R ∘ₗ g
n : N'
⊢ (Algebra.linearMap S R) (((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) m) n) = (algebraMap S R) (g n)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x
  obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
    UniqueFactorizationMonoid.exists_reduced_factors' a b
      (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)
  obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
  refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩
  refine mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_
  simp only [map_mul, Algebra.smul_def] at *
  rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module L M
inst✝⁹ : Module L N
inst✝⁸ : Module K M
inst✝⁷ : Module K N
inst✝⁶ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝⁵ : p.IsPerfPair
M' : Type u_5
N' : Type u_6
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup N'
inst✝² : Module K M'
inst✝¹ : Module K N'
inst✝ : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl (span L ↑i.range) (span L ↑j.range)
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap K L).range
this : (p.compl₁₂ (span L (Set.range ⇑i)).subtype (span L (Set.range ⇑j)).subtype).IsPerfPair
⊢ span L ↑(Submodule.inclusionSpan L j.range ∘ₗ j.rangeRestrict).range = ⊤

Tactic:
by rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range j).span_range_inclusionSpan L

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
obtain ⟨s, hs⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

Tactic:
let b := Module.Free.chooseBasis R M

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
left✝ : IsNoetherian R R
right✝ : IsArtinian R R
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

Tactic:
let b := Module.Free.chooseBasis R M

Goal state after:
case neg.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b✝ : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
left✝ : IsNoetherian R R
right✝ : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)
hy : (algebraMap O F) y ≠ 0
⊢ v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ 1

Tactic:
grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝ ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a✝

Tactic:
use 1

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝¹ : ValueGroup A K
a✝ : K
⊢ 1 • a✝ = a✝
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inr
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
hv : v.Integers O
inst✝ : Subsingleton (↥(MonoidHom.mrange v))ˣ
x : F
hx : x ≠ 0
⊢ v x ≤ 1

Tactic:
· exact (congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ)
      ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
ha : Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≠ 0
⊢ (MulAction.orbitRel Aˣ K) (a * a⁻¹) 1

Tactic:
use 1

Goal state after:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
ha : Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≠ 0
⊢ (fun m ↦ m • 1) 1 = a * a⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk.mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
d : A
hd : (algebraMap A K) d * b = c ∨ a = 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

Tactic:
obtain rfl | rfl := hd

Goal state after:
case mk.mk.mk.inl
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
d : A
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) d * b) ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

case mk.mk.mk.inr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
d : A
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) 0 ≤ 0
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
by
  constructor
  · intro RDVR
    rcases id RDVR with ⟨Rlocal⟩
    constructor
    · assumption
    use IsLocalRing.maximalIdeal R
    constructor
    · exact ⟨Rlocal, inferInstance⟩
    · rintro Q ⟨hQ1, hQ2⟩
      obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
      have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp
      rw [submodule_span_eq, span_singleton_prime hq] at hQ2
      replace hQ2 := hQ2.irreducible
      rw [irreducible_iff_uniformizer] at hQ2
      exact hQ2.symm
  · rintro ⟨RPID, Punique⟩
    have : IsLocalRing R := IsLocalRing.of_unique_nonzero_prime Punique
    refine { not_a_field' := ?_ }
    rcases Punique with ⟨P, ⟨hP1, hP2⟩, _⟩
    have hPM : P ≤ maximalIdeal R := le_maximalIdeal hP2.1
    order

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
x y : M
⊢ ⟨fun n ↦ (f n) (x + y), ⋯⟩ = ⟨fun n ↦ (f n) x, ⋯⟩ + ⟨fun n ↦ (f n) y, ⋯⟩

Tactic:
simp only [map_add]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
x y : M
⊢ ⟨fun n ↦ (f n) x + (f n) y, ⋯⟩ = ⟨fun n ↦ (f n) x, ⋯⟩ + ⟨fun n ↦ (f n) y, ⋯⟩
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ (addVal R) (ϖ ^ n) = ↑n

Tactic:
rw [addVal_pow, addVal_uniformizer h, nsmul_one]

Goal state after: