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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
β : Weight K (↥H) L
hβ : β.IsNonZero
y g : L
hy : y ∈ genWeightSpace L ⇑β
hg : g ∈ rootSpace H ⇑β
hg_ne_zero : g ≠ 0
⊢ ⟨g, hg⟩ ≠ 0

Tactic:
ne_eq,

Goal state after:
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
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
hx : x ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
β : Weight K (↥H) L
hβ : β.IsNonZero
y g : L
hy : y ∈ genWeightSpace L ⇑β
hg : g ∈ rootSpace H ⇑β
hg_ne_zero : g ≠ 0
⊢ ¬⟨g, hg⟩ = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : 2 * S R (↑n + 1 + 1) = X * S R (↑n + 1) + C R (↑n + 1 + 1)
ih2 : 2 * S R (↑n + 1) = X * S R ↑n + C R (↑n + 1)
⊢ 2 * S R (↑n + 2 + 1) = X * S R (↑n + 2) + C R (↑n + 2 + 1)

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
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 (T R (↑n + 1)) = T R' (↑n + 1)
ih2 : map f (T R ↑n) = T R' ↑n
⊢ map f (T R (↑n + 2)) = T R' (↑n + 2)

Tactic:
| add_two n ih1 ih2 =>

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 y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (↑m + 1)) x =
    (Polynomial.eval t (S R (↑m + 1)) + Polynomial.eval t (S R (↑m + 1 - 1))) • x +
      (Polynomial.eval t (S R (↑m + 1 - 1)) * -g x) • y

Tactic:
rw [add_comm (m : ℤ) 1, zpow_one_add, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ ↑m) x =
    (Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x + (Polynomial.eval t (S R (↑m - 1)) * -g x) • y
⊢ (reflection hf)
      ((reflection hg)
        ((Polynomial.eval t (S R ↑m) + Polynomial.eval t (S R (↑m - 1))) • x +
          (Polynomial.eval t (S R (↑m - 1)) * -g x) • y)) =
    (Polynomial.eval t (S R (1 + ↑m)) + Polynomial.eval t (S R (1 + ↑m - 1))) • x +
      (Polynomial.eval t (S R (1 + ↑m - 1)) * -g x) • y
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 (U R (↑n + 1)) = U R' (↑n + 1)
ih2 : map f (U R ↑n) = U R' ↑n
⊢ map f (U R (↑n + 2)) = U R' (↑n + 2)

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
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 (C R (↑n + 1)) = C R' (↑n + 1)
ih2 : map f (C R ↑n) = C R' ↑n
⊢ map f (C R (↑n + 2)) = C R' (↑n + 2)

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
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 (S R (↑n + 2)) = S R' (↑n + 2)

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: case zero
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)
hmn : n - m = 0
⊢ x m = (factor ⋯) (x n)

Tactic:
rw [hmn, Nat.add_zero] at this
    subst this
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ c * c ∈ I ^ (n + 1)

Tactic:
pow_add

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ c * c ∈ I ^ n * I ^ 1
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 ≠ 0 ↔ Nontrivial M

Tactic:
ne_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ¬length R M = 0 ↔ Nontrivial M
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
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 : ¬length R N ≠ ⊤
this : ¬length R M ≠ ⊤
⊢ length R M = length R N + length R P

Tactic:
ne_eq,

Goal state after:
case neg
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 : ¬¬length R N = ⊤
this : ¬¬length R M = ⊤
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
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
⊢ length R M = length R N + length R P

Tactic:
have := mt (IsFiniteLength.of_surjective · hg) hP

Goal state after:
case neg
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
this : ¬IsFiniteLength R M
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
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 : ¬length R P ≠ ⊤
this : ¬length R M ≠ ⊤
⊢ length R M = length R N + length R P

Tactic:
ne_eq,

Goal state after:
case neg
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 : ¬¬length R P = ⊤
this : ¬¬length R M = ⊤
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c, c • b = a) → ∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c

Tactic:
· rintro ⟨e, he⟩; dsimp
          use c * e * (d⁻¹ : Aˣ)
          simp_rw [Units.smul_def, ← he, mul_smul]
          rw [← mul_smul _ _ b, Units.inv_mul, one_smul]

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

Goal state before:
pp: case mk.mk.inr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ∨
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xb / (algebraMap A K) yb) ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) ((algebraMap A K) xa / (algebraMap A K) ya)

Tactic:
left
    use c
    rw [Algebra.smul_def]
    field_simp
    simp only [← map_mul]; congr 1; linear_combination h

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

Goal state before:
pp: case mp
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ x ∈ (valuation A K).integer → ∃ a, (algebraMap A K) a = x

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case mp
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ ∃ a, (algebraMap A K) a = c • 1
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ (∃ a, (algebraMap A K) a = x) → x ∈ (valuation A K).integer

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case mpr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ (algebraMap A K) c ∈ (valuation A K).integer
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
⊢ ¬DenselyOrdered ↑(range ⇑v)

Tactic:
intro H
  -- nonunits as an ideal isn't defined here, nor shown to be equivalent to `v x < 1`
  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
  }
  obtain ⟨x, hx₁, hx⟩ :
    ∃ x, v (algebraMap O F x) < 1 ∧
      v (algebraMap O F x) ∈ upperBounds (Iio 1 ∩ range (v ∘ algebraMap O F)) := by
    simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range]
      using IsPrincipalIdealRing.principal I
  obtain ⟨y, hy, hy₁⟩ : ∃ y, v (algebraMap O F x) < v y ∧ v y < 1 := by
    simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁
  obtain ⟨z, rfl⟩ := hv.exists_of_le_one hy₁.le
  exact hy.not_ge <| hx ⟨hy₁, mem_range_self _⟩

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 : AdicCompletion I M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ ↑x n = ↑0 n

Tactic:
refine smul_induction_on (SModEq.zero.1 <| h n) (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
    · simp only [val_smul_apply, val_zero]
      induction x.val n using Quotient.inductionOn' with | _ a
      exact SModEq.zero.2 <| smul_mem_smul hr mem_top
    · simp only [val_add_apply, hx, val_zero_apply, hy, add_zero]

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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n : ℕ
⊢ ↑((mk I M) f) n = ↑0 n

Tactic:
obtain ⟨m, hnm, l, hnl, hl⟩ := h (n + k) (by lia)

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ ↑((mk I M) f) n = ↑0 n
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_2
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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
I : Ideal R
x✝ : I ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hI : Ideal.comap (algebraMap R S) P' ≤ I
hIm : I.IsMaximal
hyI : y ∉ I
⊢ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I

Tactic:
· exact IsLocalization.under_map_of_isPrime_disjoint _ S hIm.isPrime <|
      (disjoint_powers_iff_notMem_of_isPrime y).2 hyI

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v

Tactic:
· apply (hirr.ne_zero (eq_zero_of_pow_eq_zero h)).elim

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
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
obtain ⟨x, hx : _ = Ideal.span _⟩ := h'

Goal state after:
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}
⊢ ∃ n, I = maximalIdeal R ^ n
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ (restrict₀ (ofClass v)) x ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
⊢ ¬(restrict₀ (ofClass v)) x = 0
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
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ IsPrincipal.generator I ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ ¬IsPrincipal.generator I = 0
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : NonUnitalCommSemiring T
s : T
⊢ s ∈ sumSq T ↔ IsSumSq s

Tactic:
simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]

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

Goal state before:
pp: case neg.hxy
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 y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hy'.choose).2 * (ofClass v) (↑hx'.choose).1 ≠ 0

Tactic:
simpa only [MonoidWithZeroHom.coe_ofClass, ← map_mul v, ne_eq, h.eq_zero, map_mul w]
          using mul_ne_zero hx10 hy20

Goal state after:
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
p : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ (preReflection (root i) (p.flip (coroot i))) ((preReflection (root i) (p.flip (coroot i))) (root j)) = root j

Tactic:
apply involutive_preReflection (x := root i) (hp i)

Goal state after:
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 y : (ofClass v).ValueGroup₀
⊢ h.valueGroup₀Fun x ≤ h.valueGroup₀Fun y ↔ x ≤ y

Tactic:
by
    simp only [valueGroup₀Fun, ne_eq]
    split_ifs with hx0 hy0 hy0
    · simp [hx0, hy0]
    · simp [hx0]
    · simp [hx0, hy0]
    · generalize_proofs _ _ _ _ hx _ _ hy
      conv_rhs => rw [hx.choose_spec, hy.choose_spec]
      simp only [valueGroup.mk, WithZero.coe_le_coe, Subtype.mk_le_mk]
      nth_rw 2 [mul_comm]
      rw [le_mul_inv_iff_mul_le, mul_assoc, mul_comm, ← le_mul_inv_iff_mul_le, inv_inv]
      nth_rw 4 [mul_comm]
      conv_rhs =>
        rw [le_mul_inv_iff_mul_le, mul_assoc, mul_comm, ← le_mul_inv_iff_mul_le, inv_inv]
      generalize_proofs _ hx' hx20 hy' hy10 hx10 hy20
      rw [← Units.mk0_mul _ _ (mul_ne_zero hx10 hy20), ← Units.mk0_mul _ _ (mul_ne_zero hx20 hy10),
        ← Units.mk0_mul, ← Units.mk0_mul]
      · simp only [← Units.val_le_val]
        repeat rw [Units.val_mk0]
        simp only [MonoidWithZeroHom.coe_ofClass, ← map_mul w, ← h.le_iff_le]
        simp
      · simpa only [MonoidWithZeroHom.coe_ofClass, ← map_mul v, ne_eq, h.eq_zero, map_mul w]
          using mul_ne_zero hx10 hy20
      · simpa only [MonoidWithZeroHom.coe_ofClass, ← map_mul v, ne_eq, h.eq_zero, map_mul w]
          using mul_ne_zero hx20 hy10

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
inst✝ : Fintype ι
⊢ (P.Polarization.domRestrict (P.rootSpan R)).range ≤ P.corootSpan R

Tactic:
by
  intro y hy
  obtain ⟨x, hx⟩ := hy
  rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]
  refine (Submodule.mem_span_range_iff_exists_fun R).mpr ?_
  use fun i => P.toLinearMap x (P.coroot i)
  simp

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✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
⊢ (P.PolarizationIn S).range ≤ P.corootSpan S

Tactic:
by
  intro x hx
  obtain ⟨y, hy⟩ := hx
  rw [PolarizationIn_apply] at hy
  exact (Submodule.mem_span_range_iff_exists_fun S).mpr
    (Exists.intro (fun i ↦ (P.coroot'In S i) y) hy)

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

Goal state before:
pp: case mpr.mp.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:
rw [show x = -1 + (1 + x) by simp]

Goal state after:
case mpr.mp.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' (-1 + (1 + x)) ≤ 1