mathlib-initiative/mathlib-tactics huggingface dataset:
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
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R ↥⊤ ∧ IsArtinian R M

Tactic:
← Submodule.topEquiv.isArtinian_iff,

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
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R ↥⊤ ∧ IsArtinian R ↥⊤
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
⊢ f (-1) ^ Nat.succ 1 = 1

Tactic:
← map_pow,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
⊢ f ((-1) ^ Nat.succ 1) = 1
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsFiniteLength R M
⊢ length R M ≠ ⊤

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp H

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : IsFiniteLength R M
s : CompositionSeries (Submodule R M)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
⊢ length R M ≠ ⊤
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing S
inst✝³ : Module S M
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ (I ^ n • ⊤).toAddSubgroup ≤ (J ^ n • ⊤).toAddSubgroup

Tactic:
← AddSubgroup.toAddSubmonoid_le

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing S
inst✝³ : Module S M
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
x : M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ (I ^ n • ⊤).toAddSubgroup.toAddSubmonoid ≤ (J ^ n • ⊤).toAddSubgroup.toAddSubmonoid
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
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
⊢ False

Tactic:
set I : Ideal O := {
    carrier := v ∘ algebraMap O F ⁻¹' Iio (1 : Γ₀)
    add_mem' := fun {a b} ha hb ↦ by simpa using map_add_lt v ha hb
    zero_mem' := by simp
    smul_mem' := by
      intro c x
      simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, map_mul]
      intro hx
      exact Right.mul_lt_one_of_le_of_lt (hv.map_le_one c) hx
  }

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ False
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
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
constructor
  · intro H x
    obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x
    have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
    obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
    · exact Or.inr
        ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩
    · exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩
  · intro H
    suffices PreValuationRing R from mk
    constructor
    intro a b
    by_cases ha : a = 0; · subst ha; exact ⟨0, Or.inr <| mul_zero b⟩
    by_cases hb : b = 0; · subst hb; exact ⟨0, Or.inl <| mul_zero a⟩
    replace ha := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr ha
    replace hb := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr hb
    obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)
    · rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
      exact ⟨c, Or.inr e⟩
    · rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e
      exact ⟨c, Or.inl e⟩

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
inst✝⁷ : SMul S T
inst✝⁶ : SMul S R
inst✝⁵ : SMul T R
inst✝⁴ : SMul S M
inst✝³ : SMul T M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower T R M
inst✝ : IsScalarTower S T M
s : S
t : T
f : AdicCompletion I M
⊢ (s • t) • f = s • t • f

Tactic:
ext; simp [val_smul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
⊢ Submodule.IsPrincipal I

Tactic:
by_cases I0 : I = ⊥

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : I = ⊥
⊢ Submodule.IsPrincipal I

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
⊢ Submodule.IsPrincipal I
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n
⊢ ⇑F = ⇑(lift I ha f ⋯)

Tactic:
apply IsHausdorff.StrictMono.funext I ha

Goal state after:
R : Type u_1
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n
⊢ ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (F m) = Submodule.Quotient.mk ((lift I ha f ⋯) m)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ x ∈ ⊥.jacobson

Tactic:
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ ∀ (y : R), IsUnit (-x * y + 1)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
⊢ ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]

Tactic:
intro m n h

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hxy✝ : x * y ∈ under R P'
hxy : y ∈ under R P'
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Subsingleton R
v : Valuation R Γ₀
x : R
⊢ v x ≤ 1

Tactic:
by
  rw [Subsingleton.elim x 1, Valuation.map_one]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (x + y) = v x

Tactic:
rw [add_comm]; exact map_add_eq_of_lt_right _ h

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
⊢ v (x - y) = v y

Tactic:
by
  by_cases hy : v y = 0
  · simpa [*] using map_sub v x y
  · simp [*, map_sub_eq_of_lt_right, zero_lt_iff]

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

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
⊢ ∃ n, Associated (x ^ n) (fa ::ₘ fs).prod

Tactic:
obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)

Goal state after:
case cons.inr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ ∃ n, Associated (x ^ n) (fa ::ₘ fs).prod
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case top
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ OrderDual.toDual ((addVal R) (generator (ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ⊤))) = OrderDual.toDual ⊤

Tactic:
| top =>

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * ↑u ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ∈ maximalIdeal R

Tactic:
exact (H _).mpr (dvd_refl _)

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

Goal state before:
pp: case top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : (addVal R) y = vy
hvx : (addVal R) x = ⊤
⊢ ⊤ ≤ vy ↔ x ∣ y

Tactic:
| top =>

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

Goal state before:
pp: case coe.top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : (addVal R) x = ↑vx
hvy : (addVal R) y = ⊤
⊢ ↑vx ≤ ⊤ ↔ x ∣ y

Tactic:
| top =>

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
this : ⊥.IsMaximal
⊢ ⊥.IsMaximal

Tactic:
rw [← IsLocalization.under_map_of_isPrime_disjoint M (Localization M) isPrime_bot
      (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
this : ⊥.IsMaximal
⊢ (under (R ⧸ P') (Ideal.map (algebraMap (R ⧸ P') (Localization M)) ⊥)).IsMaximal
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
⊢ (algebraMap R (T ⧸ P)).IsIntegral

Tactic:
let w : (S[X] ⧸ Q) ≃ₐ[R] (T ⧸ P) := Ideal.quotientEquivAlg Q P v hw.symm

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
⊢ (algebraMap R (T ⧸ P)).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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✝ : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ ∑ i, (P.coroot' i) ↑x • P.coroot i ∈ P.corootSpan R

Tactic:
refine (Submodule.mem_span_range_iff_exists_fun R).mpr ?_

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✝ : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ ∃ c, ∑ i, c i • P.coroot i = ∑ i, (P.coroot' i) ↑x • P.coroot i
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v' x ≤ 1
hx' : v' x < 1
⊢ v' (1 + x) = 1

Tactic:
← v'.map_one

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
hx : v' x ≤ 1
hx' : v' x < 1
⊢ v' (1 + x) = v' 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).1 = ((id.prodMap (Module.Dual.eval R M)) x).1

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).2 = ((id.prodMap (Module.Dual.eval R M)) x).2

Tactic:
· ext
      dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
      simp

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).2 = ((id.prodMap (Module.Dual.eval R M)) x).2
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
x : Module.Dual R M × M
⊢ (h_d x).2 = ((id.prodMap (Module.Dual.eval R M)) x).2

Tactic:
· ext
      dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
      simp

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff'.mpr fun s c hc ↦ ?_

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
⊢ ∀ i ∈ s, c i = 0
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Semiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g⁻¹) ((ρ g) x) = x

Tactic:
by
  simp [← Module.End.mul_apply, ← map_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Semiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ (ρ g) ((ρ g⁻¹) x) = x

Tactic:
by
  simp [← Module.End.mul_apply, ← map_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : (ofModule M).asModule
⊢ (RestrictScalars.addEquiv k k[G] M) ((ofModule M).asModuleEquiv (r • m)) =
    r • (RestrictScalars.addEquiv k k[G] M) ((ofModule M).asModuleEquiv m)

Tactic:
by
  dsimp
  simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]

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

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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
⊢ ∃ Φ, (∀ i ∈ Φ, ¬Disjoint q (R ∙ P.root i)) ∧ ∀ i ∉ Φ, q ≤ ker (P.coroot' i)

Tactic:
refine ⟨{i | ¬ Disjoint q (R ∙ P.root i)}, by simp, fun i hi ↦ ?_⟩

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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
i : ι
hi : i ∉ {i | ¬Disjoint q (R ∙ P.root i)}
⊢ q ≤ ker (P.coroot' i)