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

Goal state before:
pp: case lie.a.a.a.a.a.a.a.a
ι : 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
x yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yl, zc⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ T R 0 = 1

Tactic:
simp [T]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ T R 1 = X

Tactic:
simp [T]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank K ↥(rootSpace H ⇑α)
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
F : ↥(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H ⇑α
hy₀ : ⟨y, hyα⟩ ≠ 0
hy : ⁅y, f⁆ = 0
P : ⋯.HasPrimitiveVectorWith y (-2)
⊢ False

Tactic:
obtain ⟨n, hn⟩ := P.exists_nat

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
contra : 1 < finrank K ↥(rootSpace H ⇑α)
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
F : ↥(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H ⇑α
hy₀ : ⟨y, hyα⟩ ≠ 0
hy : ⁅y, f⁆ = 0
P : ⋯.HasPrimitiveVectorWith y (-2)
n : ℕ
hn : -2 = ↑n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp (Polynomial.C 1 * X) = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
map_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp (1 * X) = Polynomial.C 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
⊢ T R n = Polynomial.C 1 * T R n

Tactic:
map_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
⊢ T R n = 1 * T R n
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅↑h, e⁆ = α h • e
hf_wt : ⁅↑h, f⁆ = (-α) h • f
hef_zero : ⁅↑h, ⁅e, f⁆⁆ = 0
⊢ ∃ c₁_1 c₂_1 c₃_1, c₁ • ⁅↑h, e⁆ + c₂ • ⁅↑h, f⁆ + c₃ • ⁅↑h, ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆

Tactic:
exact ⟨c₁ * α h, c₂ * (-α h), 0, by simp [he_wt, hf_wt, hef_zero, smul_smul]⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (Polynomial.C 1 * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
map_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (1 * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ ↑↑(corootSpace ⇑α)
x_pos : L
hx_pos : x_pos ∈ ↑(genWeightSpace L ⇑α)
x_neg : L
hx_neg : x_neg ∈ ↑(genWeightSpace L (-⇑α))
hx_αneg : x_pos + x_neg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
hx : x_pos + x_neg + ↑H.toLieSubmodule.incl y ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ x_pos + x_neg + ↑H.toLieSubmodule.incl y ∈ sl2SubmoduleOfRoot hα

Tactic:
obtain ⟨c₁, rfl⟩ := aux hα hx_pos heα ht.e_ne_zero

Goal state after:
case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
aux :
  ∀ {β : Weight K (↥H) L},
    β.IsNonZero → ∀ {y g : L}, y ∈ genWeightSpace L ⇑β → g ∈ rootSpace H ⇑β → g ≠ 0 → ∃ c, y = c • g
y : ↥H.toLieSubmodule
hy_coroot : y ∈ ↑↑(corootSpace ⇑α)
x_neg : L
hx_neg : x_neg ∈ ↑(genWeightSpace L (-⇑α))
c₁ : K
hx_pos : c₁ • e ∈ ↑(genWeightSpace L ⇑α)
hx_αneg : c₁ • e + x_neg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
hx : c₁ • e + x_neg + ↑H.toLieSubmodule.incl y ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
⊢ c₁ • e + x_neg + ↑H.toLieSubmodule.incl y ∈ sl2SubmoduleOfRoot hα
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
⊢ sl2SubmoduleOfRoot hα ≠ ⊥

Tactic:
sl2SubmoduleOfRoot_eq_sup

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
⊢ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α ≠ ⊥
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.root' i) (P.coroot j - (P.toLinearMap (P.root j)) (P.coroot j) • P.coroot j) = -P.pairing i j

Tactic:
root_coroot_eq_pairing,

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
i j : ι
⊢ (P.root' i) (P.coroot j - P.pairing j j • P.coroot j) = -P.pairing i j
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h₁ := congr_arg derivative <| one_sub_X_sq_mul_derivative_T_eq_poly_in_T (R := R) (n - 1)

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  derivative ((1 - X ^ 2) * derivative (T R (n - 1 + 1))) =
    derivative ((↑(n - 1) + 1) * (T R (n - 1) - X * T R (n - 1 + 1)))
⊢ (1 - X ^ 2) * (⇑derivative)^[2] (T R n) = X * derivative (T R n) - ↑n ^ 2 * T R n
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id + (↑n • LinearMap.smulRight (f - g) x + LinearMap.smulRight (f - g) x) =
    LinearMap.id + (↑n + 1) • LinearMap.smulRight (f - g) x

Tactic:
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id + (↑n • LinearMap.smulRight (f - g) x + LinearMap.smulRight (f - g) x) =
    LinearMap.id + (↑n • LinearMap.smulRight (f - g) x + 1 • LinearMap.smulRight (f - g) x)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
by
  have h := congr_arg derivative <| add_one_mul_T_eq_poly_in_U (R := R) n
  simp only [derivative_add, derivative_sub, derivative_mul, derivative_X, derivative_one,
    derivative_X_pow, derivative_intCast, C_eq_natCast, T_derivative_eq_U] at h
  rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
  linear_combination (norm := (push_cast; ring_nf)) h

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

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

Tactic:
mul_comm (X ^ 2),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative)^[k + 2] (T R n) - (⇑derivative)^[k] ((⇑derivative)^[2] (T R n) * X ^ 2) =
    (⇑derivative)^[k] (X * derivative (T R n) - ↑(n ^ 2) * T R n)
⊢ (1 - X ^ 2) * (⇑derivative)^[k + 2] (T R n) =
    (2 * ↑k + 1) * X * (⇑derivative)^[k + 1] (T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑derivative)^[k] (T R n)
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] (X ^ 2 * (⇑derivative)^[2] (U R n)) =
    (⇑derivative)^[k] (3 * X * derivative (U R n) - ↑((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_comm (X ^ 2),

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) - ↑((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.RingTheory.Polynomial.Chebyshev

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

Tactic:
rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] at h

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (T R n)) = -((↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (T R n)) = -(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] at h

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h : eval 0 ((⇑derivative)^[k + 2] (U R n)) = -(((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n)))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) = -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case left
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * (algebraMap A K) 1

Tactic:
map_one,

Goal state after:
case left
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]
hp : p.Monic
r : K
hr : (aeval r) p = 0
inv : A
h_inv : 1 = ↑(den A r) * inv
d_ne_zero : (algebraMap A K) ↑(den A r) ≠ 0
⊢ (algebraMap A K) (num A r) = (algebraMap A K) (num A r) * 1
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
⊢ finrank K ↥M' = finrank L M

Tactic:
by
  obtain ⟨n, b, b', hb⟩ := exists_basis_basis_of_span_eq_top_of_mem_algebraMap p M' N' hM hN hp
  rw [finrank_eq_card_basis b, finrank_eq_card_basis b']

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
x y : { N // N.FG }
e : f x = f y
⊢ x = y

Tactic:
ext1

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
x y : { N // N.FG }
e : f x = f y
⊢ ↑x = ↑y
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
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) r1 * (algebraMap O R) r2 = (algebraMap O R) 1

Tactic:
map_one,

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
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) r1 * (algebraMap O R) r2 = 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
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) r2 * (algebraMap O R) r1 = (algebraMap O R) 1

Tactic:
map_one,

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
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) r2 * (algebraMap O R) r1 = 1
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
⊢ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Tactic:
refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩

Goal state after:
case mp.refine_1
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
⊢ (⇑v ∘ ⇑(algebraMap O F)) x ∈ ⇑v ∘ ⇑(algebraMap O F) '' ↑I

case mp.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
⊢ (⇑v ∘ ⇑(algebraMap O F)) x ∈ upperBounds (⇑v ∘ ⇑(algebraMap O F) '' ↑I)
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
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ⟨(algebraMap A K) (x✝¹ * x✝), ⋯⟩ = ⟨(algebraMap A K) x✝¹, ⋯⟩ * ⟨(algebraMap A K) x✝, ⋯⟩

Tactic:
ext1

Goal state after:
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✝¹ x✝ : A
⊢ ↑⟨(algebraMap A K) (x✝¹ * x✝), ⋯⟩ = ↑(⟨(algebraMap A K) x✝¹, ⋯⟩ * ⟨(algebraMap A K) x✝, ⋯⟩)
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
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ↑⟨(algebraMap A K) (x✝¹ * x✝), ⋯⟩ = ↑(⟨(algebraMap A K) x✝¹, ⋯⟩ * ⟨(algebraMap A K) x✝, ⋯⟩)

Tactic:
exact (algebraMap A K).map_mul _ _

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
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ⟨(algebraMap A K) 0, ⋯⟩ = 0

Tactic:
ext1

Goal state after:
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
⊢ ↑⟨(algebraMap A K) 0, ⋯⟩ = ↑0
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
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ⟨(algebraMap A K) (x✝¹ + x✝), ⋯⟩ = ⟨(algebraMap A K) x✝¹, ⋯⟩ + ⟨(algebraMap A K) x✝, ⋯⟩

Tactic:
ext1

Goal state after:
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✝¹ x✝ : A
⊢ ↑⟨(algebraMap A K) (x✝¹ + x✝), ⋯⟩ = ↑(⟨(algebraMap A K) x✝¹, ⋯⟩ + ⟨(algebraMap A K) x✝, ⋯⟩)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
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 : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝¹ : x ∈ ⊤
x✝ : M ⧸ I ^ n • ⊤
⊢ r • x✝ = 0 n

Tactic:
induction x.val n using Quotient.inductionOn' with

Goal state after:
case refine_1.h
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 : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
a : M
⊢ r • Quotient.mk'' a = 0 n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsPrecomplete I M → Function.Surjective ⇑(of I M)

Tactic:
· intro h u
    choose x hx using (fun n ↦ Submodule.Quotient.mk_surjective (I ^ n • ⊤ : Submodule R M) (u.1 n))
    obtain ⟨a, ha⟩ := h.prec (f := x) (fun hmn ↦ by rw [SModEq, hx, ← u.2 hmn, ← hx]; simp)
    use a
    ext n
    simpa [SModEq, ← eval_of, ha, ← hx] using (ha n).symm

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
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
⊢ of I N ∘ₗ lift I f ⋯ = AdicCompletion.lift I f ⋯

Tactic:
ext1

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
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x✝ : M
⊢ (of I N ∘ₗ lift I f ⋯) x✝ = (AdicCompletion.lift I f ⋯) x✝