mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-↑n)) = C R' (-↑n)
ih2 : map f (C R (-↑n + 1)) = C R' (-↑n + 1)
⊢ map f (X * C R (-↑n) - C R (-↑n + 1)) = X * C R' (-↑n) - C R' (-↑n + 1)

Tactic:
Polynomial.map_sub,

Goal state after:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-↑n)) = C R' (-↑n)
ih2 : map f (C R (-↑n + 1)) = C R' (-↑n + 1)
⊢ map f (X * C R (-↑n)) - map f (C R (-↑n + 1)) = X * C R' (-↑n) - C R' (-↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (↑n + 1)) = S R' (↑n + 1)
ih2 : map f (S R ↑n) = S R' ↑n
⊢ map f (X * S R (↑n + 1) - S R ↑n) = X * S R' (↑n + 1) - S R' ↑n

Tactic:
Polynomial.map_sub,

Goal state after:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (↑n + 1)) = S R' (↑n + 1)
ih2 : map f (S R ↑n) = S R' ↑n
⊢ map f (X * S R (↑n + 1)) - map f (S R ↑n) = X * S R' (↑n + 1) - S R' ↑n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-↑n)) = S R' (-↑n)
ih2 : map f (S R (-↑n + 1)) = S R' (-↑n + 1)
⊢ map f (X * S R (-↑n) - S R (-↑n + 1)) = X * S R' (-↑n) - S R' (-↑n + 1)

Tactic:
Polynomial.map_sub,

Goal state after:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-↑n)) = S R' (-↑n)
ih2 : map f (S R (-↑n + 1)) = S R' (-↑n + 1)
⊢ map f (X * S R (-↑n)) - map f (S R (-↑n + 1)) = X * S R' (-↑n) - S R' (-↑n + 1)
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 : ℤ
⊢ (aeval ((algebraMap R R') x)) (U R n) = eval ((algebraMap R R') x) (U R' n)

Tactic:
aeval_U

Goal state after:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ eval ((algebraMap R R') x) (U R' n) = eval ((algebraMap R R') x) (U R' n)
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 ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
g : ↥H → R
hg : g ∈ sV
⊢ g ≠ 0

Tactic:
contra

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 ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
g : ↥H → R
hg : g ∈ sV
contra : g = 0
⊢ False
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 : ι
inst✝ : NeZero 2
h : P.root i = 0
⊢ 0 = 2

Tactic:
by simpa [h] using P.root_coroot_two i

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n + 1] y = y + (n + 1) • (f y • x - 2 • y)

Tactic:
simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
      LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
      map_nsmul, map_smul, smul_neg, hz, add_smul]

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
hz : ∀ (z : M), f y • g x • z = 2 • 2 • z
⊢ f y • x - y +
      (-(n • f y • x) - (n • y + n • y + (n • y + n • y) - (n • f y • x + n • f y • x + (n • f y • x + n • f y • x))) -
        (n • f y • x - n • y + (n • f y • x - n • y))) =
    y + (n • f y • x + 1 • f y • x - (n • y + 1 • y + (n • y + 1 • y)))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (↑k + 1) = T R (m + (↑k + 1)) + T R (m - (↑k + 1))
ih2 : 2 * T R m * T R ↑k = T R (m + ↑k) + T R (m - ↑k)
h₁ : T R (m + ↑k + 2) = 2 * X * T R (m + ↑k + 1) - T R (m + ↑k)
⊢ 2 * T R m * T R (↑k + 2) = T R (m + (↑k + 2)) + T R (m - (↑k + 2))

Tactic:
have h₂ := T_sub_two R (m - k)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (↑k + 1) = T R (m + (↑k + 1)) + T R (m - (↑k + 1))
ih2 : 2 * T R m * T R ↑k = T R (m + ↑k) + T R (m - ↑k)
h₁ : T R (m + ↑k + 2) = 2 * X * T R (m + ↑k + 1) - T R (m + ↑k)
h₂ : T R (m - ↑k - 2) = 2 * X * T R (m - ↑k - 1) - T R (m - ↑k)
⊢ 2 * T R m * T R (↑k + 2) = T R (m + (↑k + 2)) + T R (m - (↑k + 2))
Module: Mathlib.Algebra.Order.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
⊢ StrictMono ⇑embedding

Tactic:
intro x y hxy

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : f.ValueGroup₀
hxy : x < y
⊢ embedding x < embedding y
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
s : CompositionSeries (Submodule R M)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
⊢ length R M ≠ ⊤

Tactic:
rw [← length_compositionSeries s hs₁ hs₂]

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 = ⊤
⊢ ↑s.length ≠ ⊤
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ length R M = length R N + ↑s.length

Tactic:
← Module.length_compositionSeries t ht₁ ht₂,

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ length R M = ↑t.length + ↑s.length
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Finite ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
cases nonempty_fintype ι
    simp [(Finsupp.linearEquivFunOnFinite R M ι).length_eq]

Goal state after:
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✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Cardinal.toENat (Module.rank R M) * length R R = ↑(finrank R M) * length R R

Tactic:
Cardinal.toENat_eq_natCast.mpr (finrank_eq_rank _ _).symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ ↑(finrank R M) * length R R = ↑(finrank 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
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
c x : O
⊢ x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1 → c • x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1

Tactic:
simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, map_mul]

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)
c x : O
⊢ v ((algebraMap O F) x) < 1 → v ((algebraMap O F) c) * v ((algebraMap O F) x) < 1
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
x y : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((↑x + ↑y) n) = (↑x + ↑y) m

Tactic:
simp [x.property, y.property]

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
x y : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((↑x - ↑y) n) = (↑x - ↑y) m

Tactic:
simp [x.property, y.property]

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

Goal state before:
pp: case inr
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
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
· rw [sup_eq_left.mpr h]; exact ⟨⟨_, rfl⟩⟩

Goal state after:
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
p : AdicCompletion I M → Prop
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
f : AdicCauchySequence I M
⊢ p ((mk I M) f)

Tactic:
exact h f

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 4 := iff_ideal_total

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
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✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m

Tactic:
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)

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:
rw [addVal_eq_top_iff] at hvy

Goal state after:
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 : y = 0
⊢ ↑vx ≤ ⊤ ↔ x ∣ y
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [ne_bot]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: 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

Tactic:
exact (toWithBotNat_le_toWithBotNat_iff hx hy).mp hle

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ v.restrict x < 1 ↔ v x < 1

Tactic:
rw [restrict_lt_iff_lt_embedding, map_one]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ i, S i)) (↥(S i)) K
val✝ : K
hin : val✝ ∈ S i
hy : (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ = x
⊢ x ∈ S i

Tactic:
← hy

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)
x : K
hx : IsIntegral (↥(⨅ i, S i)) x
i : ι
le : ⨅ i, S i ≤ S i
algInst✝ : Algebra ↥(⨅ i, S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ i, S i)) (↥(S i)) K
val✝ : K
hin : val✝ ∈ S i
hy : (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ = x
⊢ (algebraMap (↥(S i)) K) ⟨val✝, hin⟩ ∈ S i
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X), h (f x) = g x) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
rTensor_injective_iff_lcomp_surjective,

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X), h (f x) = g x) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Surjective ⇑(lcomp R (CharacterModule M) f)
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))

Tactic:
rTensor_injective_iff_lcomp_surjective,

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩) ↔
    ∀ (I : Ideal R), Surjective ⇑(lcomp R (CharacterModule M) (Submodule.subtype I))
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : (ofClass w).ValueGroup₀
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x

Tactic:
by
    obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
    · simp_all [valueGroup₀Fun_zero]
    rw [valueGroup₀Fun_spec h.symm, valueGroup₀Fun_spec h]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
⊢ IsSMulRegular M r

Tactic:
have h := Flat.rTensor_preserves_injective_linearMap (M := M)
    (toSpanSingleton R R r) <| hr.right
  -- But precomposing and postcomposing with the isomorphism `M ≃ₗ[R] (R ⊗[R] M)`
  -- we get a map `M →ₗ[R] M` which is just `(r • ·)`.
  have h2 : (fun (x : M) ↦ r • x) = ((TensorProduct.lid R M) ∘ₗ
            (rTensor M (toSpanSingleton R R r)) ∘ₗ
            (TensorProduct.lid R M).symm) := by ext; simp
  -- Hence `(r • ·) : M → M` is also injective
  rw [IsSMulRegular, h2]
  simp [h, LinearEquiv.injective]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
r : R
hr : r ∈ R⁰
inst✝ : Flat R M
⊢ IsSMulRegular M r

Tactic:
apply isSMulRegular_of_isRegular

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
r : R
hr : r ∈ R⁰
inst✝ : Flat R M
⊢ IsRegular r
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ IsSumSq (∏ i ∈ I, x i)

Tactic:
simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)

Goal state after:
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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i = 2 • (P.PolarizationIn S) (P.rootSpanMem S i)

Tactic:
two_nsmul

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    (P.PolarizationIn S) (P.rootSpanMem S i) + (P.PolarizationIn S) (P.rootSpanMem S i)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case e'_3
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : CommRing R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
B : P.InvariantForm := P.toInvariantForm
lsq : ι → R := fun i ↦ (B.form (P.root i)) (P.root i)
hlsq : ∀ (i : ι), lsq i = (P.RootForm (P.root i)) (P.root i)
h₂ : lsq k = m * m * lsq i + m * n * (2 * (B.form (P.root i)) (P.root j)) + n * n * lsq j
h₃ : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
h₁ :
  (m * m * (P.pairing i j * lsq j)) • P.coroot k + (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j
⊢ lsq j • (m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j) =
    (m * (P.pairing i j * lsq j)) • P.coroot i + (n * (P.pairing j i * lsq j)) • P.coroot j

Tactic:
· module

Goal state after: