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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁴ : Finite ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝ : Fintype ι
⊢ b.symm.baseSupp = -b.baseSupp

Tactic:
let b₁ : Module.Basis ι R H :=
    (Basis.span b.linInd).map (LinearEquiv.ofEq _ _ b.coe_cartan_eq_span).symm

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁴ : Finite ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝ : Fintype ι
b₁ : Module.Basis ι R ↥H := (Basis.span ⋯).map (LinearEquiv.ofEq H.toSubmodule (Submodule.span R (range b.h)) ⋯).symm
⊢ b.symm.baseSupp = -b.baseSupp
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x : L
i : ι
⊢ b.e i ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
apply LieSubmodule.mem_iSup_of_mem (Pi.single i 1)

Goal state after:
case mem
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁶ : Finite ι
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := ⋯
x : L
i : ι
⊢ b.e i ∈ ⨆ (_ : Pi.single i 1 ≠ 0), rootSpace H (∑ i_1, Pi.single i 1 i_1 • ⇑(b.baseSupp i_1))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (T R (↑n + 1))
ih2 : eval (-x) (T R ↑n) = ↑↑(↑n).negOnePow * eval x (T R ↑n)
⊢ eval (-x) (T R (↑n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n))

pp: R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (T R (↑n + 1))
ih2 : eval (-x) (T R ↑n) = ↑↑(↑n).negOnePow * eval x (T R ↑n)
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n)) =
    ↑↑(↑n + 2).negOnePow * eval x (T R (↑n + 2))

Tactic:
· simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]
      ring_nf

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow * eval x (T R (↑n + 1))
ih2 : eval (-x) (T R ↑n) = ↑↑(↑n).negOnePow * eval x (T R ↑n)
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (T R (↑n + 1)) - eval x (T R ↑n)) =
    ↑↑(↑n + 2).negOnePow * eval x (T R (↑n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℤ
hn : ¬n = -1
⊢ (U R n).natDegree = (n + 1).natAbs - 1

Tactic:
exact natDegree_eq_of_degree_eq_some (degree_U_of_ne_neg_one R n hn)

Goal state after:
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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
hce₀ : ce ≠ 0
hcf : hf.choose = 0
⊢ False

Tactic:
exact he.choose_spec.choose_spec.1.f_ne_zero hcf

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (U R n)) = eval ((algebraMap R R') x) (U R' n)

Tactic:
by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]

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 k : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Tactic:
have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
    simp only [← coroot_reflectionPerm, hij]
  simpa only [coreflection_apply_coroot, sub_right_inj] using h

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
⊢ eval 0 ((⇑derivative)^[k + 2] (T R n)) = -(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 0
  rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] at h
  linear_combination (norm := (push_cast; ring_nf)) h

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 1 = C R (m + 1) + C R (m - 1)

Tactic:
rw [C_add_one, C_one]

Goal state after:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * X = X * C R m - C R (m - 1) + C R (m - 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))

Tactic:
have h₁ := C_add_two R (m + (-k - 1))
    have h₂ := C_sub_two R (m - (-k - 1))
    have h₃ := C_add_two R (-k - 1)
    linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case of_simple_quotient
R : Type u_1
inst✝⁷ : Ring R
M✝ : Type u_2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Submodule R M
inst✝² : IsSimpleModule R (M ⧸ S)
a✝ : IsFiniteLength R ↥S
ih : ∀ {N : Type u_3} [inst : AddCommGroup N] [inst_1 : Module R N] (e : ↥S ≃ₗ[R] N), IsFiniteLength R N
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ IsFiniteLength R N

Tactic:
have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm

Goal state after:
case of_simple_quotient
R : Type u_1
inst✝⁷ : Ring R
M✝ : Type u_2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Submodule R M
inst✝² : IsSimpleModule R (M ⧸ S)
a✝ : IsFiniteLength R ↥S
ih : ∀ {N : Type u_3} [inst : AddCommGroup N] [inst_1 : Module R N] (e : ↥S ≃ₗ[R] N), IsFiniteLength R N
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
this : IsSimpleModule R (N ⧸ Submodule.map (↑e) S)
⊢ IsFiniteLength R N
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
⊢ length R M ≠ ⊤ ↔ IsFiniteLength R M

Tactic:
refine ⟨fun h ↦ ?_, fun H ↦ ?_⟩
  · rw [length_ne_top_iff_finiteDimensionalOrder] at h
    rw [isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_iff, isArtinian_iff]
    let R : SetRel (Submodule R M) (Submodule R M) :=
      {(N₁, N₂) : Submodule R M × Submodule R M | N₁ < N₂}
    change R.inv.IsWellFounded ∧ R.IsWellFounded
    exact ⟨.of_finiteDimensional R.inv, .of_finiteDimensional R⟩
  · obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H
    rw [← length_compositionSeries s hs₁ hs₂]
    simp

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

Goal state before:
pp: case neg.inl
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : a * c = b
⊢ a * c ∈ α

Tactic:
exact Ideal.mul_mem_right _ _ h₁

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
⊢ IsBezout R

Tactic:
classical
  rw [IsBezout.iff_span_pair_isPrincipal]
  intro x y
  rw [Ideal.span_insert]
  rcases le_total (Ideal.span {x} : Ideal R) (Ideal.span {y}) with h | h
  · rw [sup_eq_right.mpr h]; exact ⟨⟨_, rfl⟩⟩
  · rw [sup_eq_left.mpr h]; exact ⟨⟨_, rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ ∃ n, Associated (p ^ n) x

Tactic:
refine ⟨Multiset.card fx, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
⊢ Associated (p ^ fx.card) x
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)

Tactic:
refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩
  · obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
    exacts [⟨a, .inl e.symm⟩, ⟨a, .inr e.symm⟩]
  · exact isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective h.1 h.2

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
⊢ (IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegralElem p

Tactic:
obtain ⟨q'', hq''⟩ := isUnit_iff_exists_inv'.1 (IsLocalization.map_units Rₘ (⟨q', hq'⟩ : M))

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ) p')
q' : R ⧸ comap C P
hq' : q' ∈ ↑(Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
hp :
  p * (algebraMap (R[X] ⧸ P) Sₘ) ↑(p', ⟨(quotientMap P C ⋯) q', ⋯⟩).2 =
    (algebraMap (R[X] ⧸ P) Sₘ) (p', ⟨(quotientMap P C ⋯) q', ⋯⟩).1
q'' : Rₘ
hq'' : q'' * (algebraMap (R ⧸ P') Rₘ) ↑⟨q', hq'⟩ = 1
⊢ (IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegralElem p
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
⊢ (addVal R) a ≤ (addVal R) b ↔ a ∣ b

Tactic:
by
  have hp := Classical.choose_spec (exists_prime R)
  constructor <;> intro h
  · by_cases ha0 : a = 0
    · rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
      rw [h]
      apply dvd_zero
    obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
    rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
      emultiplicity_le_emultiplicity_iff] at h
    exact ha.dvd.trans (h n ha.symm.dvd)
  · rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply]
    exact emultiplicity_le_emultiplicity_of_dvd_right h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : ¬x = 0
⊢ Associated x y

Tactic:
by_cases hy : y = 0

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : ¬x = 0
hy : y = 0
⊢ Associated x y

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : ¬x = 0
hy : ¬y = 0
⊢ Associated x y
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ Associated x y → (addVal R) x = (addVal R) y

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
u : Rˣ
⊢ (addVal R) x = (addVal R) (x * ↑u)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
⊢ x ∣ y

Tactic:
by_cases hy : y = 0

Goal state after:
case pos
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
hy : y = 0
⊢ x ∣ y

case neg
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
hy : ¬y = 0
⊢ x ∣ y
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := ⋯
x : K := ⋯
M : Submodule R K := ⋯
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ maximalIdeal R ≤ R ∙ y

pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := ⋯
x : K := ⋯
M : Submodule R K := ⋯
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ R ∙ y ≤ maximalIdeal R

Tactic:
· intro m hm; obtain ⟨k, hk⟩ := hb₃ m hm; rw [← hy₂, mul_comm, mul_assoc] at hk
      rw [← mul_left_cancel₀ hb₄ hk, mul_comm]; exact Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩

Goal state after:
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := ⋯
x : K := ⋯
M : Submodule R K := ⋯
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ R ∙ y ≤ maximalIdeal R
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ range ⇑(P.restrictScalars' K).root = {x | ↑x ∈ range ⇑P.root}

Tactic:
ext ⟨x, hx⟩

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
x : M
hx : x ∈ span K (range ⇑P.root)
⊢ ⟨x, hx⟩ ∈ range ⇑(P.restrictScalars' K).root ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ range ⇑P.root}
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ range ⇑(P.restrictScalars' K).coroot = {x | ↑x ∈ range ⇑P.coroot}

Tactic:
ext ⟨x, hx⟩

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
x : N
hx : x ∈ span K (range ⇑P.coroot)
⊢ ⟨x, hx⟩ ∈ range ⇑(P.restrictScalars' K).coroot ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ range ⇑P.coroot}
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case mem
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x y : M
hy : y ∈ range ⇑P.root
⊢ y ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

Tactic:
change Algebra.linearMap S R _ = _
  simp [posForm]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
⊢ h.orderMonoidIso = OrderMonoidIso.refl (ofClass v).ValueGroup₀

Tactic:
ext x
  obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
  · simp
  · simp [orderMonoidIso, valueGroup₀Fun_spec h]

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

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
⊢ P.coxeterWeight i j ≠ 4

Tactic:
intro contra
  have := P.infinite_of_linearIndependent_coxeterWeight_four hl contra
  exact not_finite ι

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (pi Q).Anisotropic → ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic

Tactic:
rintro ⟨hle, ha⟩
    intro i
    exact ⟨hle i, anisotropic_of_pi ha i⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

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✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
⊢ (reflectRoot α β).IsNonZero

Tactic:
simpa using reflectRoot_isNonZero α β <| by simpa using hβ

Goal state after: