mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
y : L
⊢ y ∈ ⨆ β, rootSpace H β

Tactic:
simp [iSup_genWeightSpace_eq_top K H L]

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 : ℕ
⊢ y ∈ {i | i ∈ s ∧ g i • ↑S i ≠ 0} → x ≠ y → (Ne on fun i ↦ (g i • ↑S i).degree) x y

Tactic:
⟨_, hy⟩

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
⊢ x ≠ y → (Ne on fun i ↦ (g i • ↑S i).degree) x y
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case hx'
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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := ⋯
⊢ ∀ y ∈ rootSpace H (-0), ((killingForm K L) (⁅e, f⁆ - ((killingForm K L) e) f • ↑α')) y = 0

Tactic:
intro z

Goal state after:
case hx'
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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
z : L
⊢ z ∈ rootSpace H (-0) → ((killingForm K L) (⁅e, f⁆ - ((killingForm K L) e) f • ↑α')) z = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (a : ℤ), motive a

Tactic:
by
  refine Chebyshev.induct motive zero one add_two ?_
  have neg' (n : ℤ) (h : motive (-n)) : motive n := by
    convert! neg (-n) h; rw [neg_neg]
  intro n h₀ h₁
  cases n with
  | zero => exact neg 1 h₁
  | succ n =>
    apply neg (n + 2) (add_two n (neg' _ h₀) (neg' n ?_))
    convert! h₁ using 1; omega

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: 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)
⊢ ∀ (z : M), f y • g x • z = 2 • 2 • z

Tactic:
intro z

Goal state after:
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)
z : M
⊢ f y • g x • z = 2 • 2 • z
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: 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
inst✝ : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
h : x + x = y + y
⊢ x = y

Tactic:
← two_zsmul,

Goal state after:
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
inst✝ : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
h : 2 • x = y + y
⊢ x = y
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (U R n) * X ^ 2) =
    (⇑derivative)^[k] (3 * X * derivative (U R n)) - (⇑derivative)^[k] (↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)

Tactic:
mul_assoc 3,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (U R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (U R n) * X ^ 2) =
    (⇑derivative)^[k] (3 * (X * derivative (U R n))) - (⇑derivative)^[k] (↑((n + 2) * n) * U R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (U R n) =
    (2 * ↑k + 3) * X * (⇑derivative)^[k + 1] (U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑derivative)^[k] (U R n)
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
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
⊢ Injective ⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp)

Tactic:
by
  let f := LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap S R)
      (FaithfulSMul.algebraMap_injective S R) p hp
  rw [← LinearMap.ker_eq_bot]
  refine (Submodule.eq_bot_iff _).mpr fun x (hx : f x = 0) ↦ ?_
  replace hx (n : N) : p (i x) n = 0 := by
    have hn : n ∈ span R (LinearMap.range j : Set N) := hN ▸ Submodule.mem_top
    induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop
  rw [← i.map_eq_zero_iff hi, ← p.map_eq_zero_iff p.toPerfPair.injective]
  ext n
  simpa using hx n

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ↑(den A r) ∣ p.leadingCoeff * num A r ^ p.natDegree

Tactic:
← coeff_scaleRoots_natDegree

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ↑(den A r) ∣ (p.scaleRoots ?s).coeff p.natDegree * num A r ^ p.natDegree

case s
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ A
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ℕ → Submodule R M
hp : Antitone p
x : (n : ℕ) → M ⧸ p n
h : ∀ (m : ℕ), x m = (factor ⋯) (x (m + 1))
m n : ℕ
g : m ≤ n
this : n = m + (n - m)
x✝ : ℕ
hmn : n - m = x✝
⊢ x m = (factor ⋯) (x n)

Tactic:
induction hmn : n - m generalizing m n with

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
c : 0 = 1
d : Aˣ
hd : (fun m ↦ m • 1) d = 0
⊢ False

Tactic:
apply_fun fun t => d⁻¹ • t at hd

Goal state after:
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
c : 0 = 1
d : Aˣ
hd : d⁻¹ • (fun m ↦ m • 1) d = d⁻¹ • 0
⊢ False
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : x ∈ {x | v x ≤ 1}
⊢ -x ∈ {x | v x ≤ 1}

Tactic:
simp only [Set.mem_ofPred_eq] at hx

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : v x ≤ 1
⊢ -x ∈ {x | v x ≤ 1}
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v 1 ≤ v ((algebraMap O R) x)

Tactic:
hvx,

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v 1 ≤ 1
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
⊢ b ∈ α

Tactic:
← h

Goal state after:
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 ∈ α
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inr
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 : b * c = a
⊢ a ∈ β

Tactic:
← h

Goal state after:
case neg.inr
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 : b * c = a
⊢ b * c ∈ β
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2

Tactic:
refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
  · obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b <;> simp
  · obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := H.total a b <;> use c <;> simp

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
⊢ Associated p ϖ

Tactic:
rcases this.isUnit_or_isUnit rfl with (H0 | H0)

Goal state after:
case inr.inr.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit ϖ
⊢ Associated p ϖ

case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ (1 + n + 1)) p
this : Irreducible (ϖ * ϖ ^ (1 + n))
H : 1 < 1 + n + 1
H0 : IsUnit (ϖ ^ (1 + n))
⊢ Associated p ϖ
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
have PID : IsPrincipalIdealRing R := aux_pid_of_ufd_of_unique_irreducible R h₁ h₂

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
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:
← sub_neg_eq_add,

Goal state after:
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
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: 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
h : ∀ r ∈ I, r = 0
⊢ False

Tactic:
apply hI

Goal state after:
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
h : ∀ r ∈ I, r = 0
⊢ I = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ
⊢ Module.length R (R ⧸ maximalIdeal R ^ n) = ↑n

Tactic:
rw [Module.length_quotient, coheight_pow_maximalIdeal]

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

Goal state before:
pp: case coe.coe
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
vy : ℕ
hvy : (addVal R) y = ↑vy
⊢ ↑vx ≤ ↑vy ↔ (addVal R) x ≤ (addVal R) y

Tactic:
hvx,

Goal state after:
case coe.coe
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
vy : ℕ
hvy : (addVal R) y = ↑vy
⊢ ↑vx ≤ ↑vy ↔ ↑vx ≤ (addVal R) y
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 v).ValueGroup₀
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x

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

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
property✝¹ : R ∙ x ∈ (Ideal R)⁰
y : R
property✝ : R ∙ y ∈ (Ideal R)⁰
⊢ ↑(⟨R ∙ x, property✝¹⟩ * ⟨R ∙ y, property✝⟩) = R ∙ x * y

Tactic:
by
      simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ ((Ideal.Quotient.mk P).comp C).IsIntegral

Tactic:
by
  change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
  apply quotient_mk_comp_C_isIntegral_of_isJacobsonRing'
  infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
x : R
⊢ C x = ((renameEquiv R e).toRingEquiv.toRingHom.comp C) x

Tactic:
exact ((renameEquiv R e).commutes' x).symm

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

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 R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ P.flip.IsValuedIn S

Tactic:
isValuedIn_iff,

Goal state after:
ι : Type u_1
R : Type u_2
S✝ : Type u_3
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 j : ι
S : Type u_6
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
⊢ ∀ (i j : ι), ∃ s, (algebraMap S R) s = P.flip.pairing i j
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁵ : CommRing K
inst✝⁴ : Field L
inst✝³ : CommRing A
inst✝² : IsJacobsonRing K
inst✝¹ : IsNoetherianRing K
inst✝ : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
⊢ f.Finite

Tactic:
algebraize [f, (g.comp f)]

Goal state after:
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁵ : CommRing K
inst✝⁴ : Field L
inst✝³ : CommRing A
inst✝² : IsJacobsonRing K
inst✝¹ : IsNoetherianRing K
inst✝ : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
algInst✝¹ : Algebra K L := f.toAlgebra
algInst✝ : Algebra K A := (g.comp f).toAlgebra
algebraizeInst✝ : Algebra.FiniteType K A
⊢ f.Finite
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr.mpr.inl
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
this : v' (1 + x) = 1
⊢ v x ≤ 1

Tactic:
← h

Goal state after:
case mpr.mpr.inl
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
this : v (1 + x) = 1
⊢ v x ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr.mpr.inr
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 x ≤ 1

Tactic:
← h

Goal state after:
case mpr.mpr.inr
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 x ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x < 1 ↔ v' x < 1) → v.IsEquiv v'

Tactic:
isEquiv_iff_val_eq_one

Goal state after:
case mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x < 1 ↔ v' x < 1) → ∀ {x : K}, v x = 1 ↔ v' x = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mp
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 : ¬x = 0
⊢ v x = 1 → v' x = 1

Tactic:
intro hh

Goal state after:
case neg.mp
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 : ¬x = 0
hh : v x = 1
⊢ v' x = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mpr
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 : ¬x = 0
⊢ v' x = 1 → v x = 1

Tactic:
intro hh

Goal state after:
case neg.mpr
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 : ¬x = 0
hh : v' x = 1
⊢ v x = 1
Module: Mathlib.LinearAlgebra.RootSystem.Basic

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
this✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.flip ∘ ⇑coroot))
⊢ MapsTo (⇑(sα ∘ₗ sβ ∘ₗ sα)) (range ⇑root) (range ⇑root)

Tactic:
exact (hr i).comp <| (hr j).comp (hr i)

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

Goal state before:
pp: case refine_2
ι : 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✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (2 • P.coroot j) = 2 • 1

Tactic:
← h

Goal state after:
case refine_2
ι : 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✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot i) = 2 • 1