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

Goal state before:
pp: case «0»
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨0, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨1, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
· exact toLieSubmodule_le_rootSpace_zero R L H

Goal state after:
case «1»
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨1, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
⊢ ![H.toLieSubmodule, b.borelLower, b.borelUpper] ((fun i ↦ i) ⟨2, ⋯⟩) ≤
    ![rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
        ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
      ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (C R 0).comp (2 * X) = 2 * T R 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (C R 0) = 2

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval (-2) (C R 0) = 2 * ↑↑(Int.negOnePow 0)

Tactic:
| zero =>

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

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

Tactic:
have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (C_comp_two_mul_X R n)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : ((C R n).comp (2 * X)).comp (Polynomial.C ⅟2 * X) = (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: case zero
R : Type u_1
inst✝ : CommRing R
⊢ S R (-0 - 1) = -S R (0 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (S R 0) = ↑0 + 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval (-2) (S R 0) = ↑↑(Int.negOnePow 0) * (↑0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (S R 0).comp (2 * X) = U R 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ S R 0 ^ 2 + S R (0 + 1) ^ 2 - X * S R 0 * S R (0 + 1) = 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ 2 * S R (0 + 1) = X * S R 0 + C R (0 + 1)

Tactic:
| zero =>

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
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
c : K
hc : c • ⟨g, hg⟩ = ⟨y, hy⟩
⊢ ∃ c, y = c • g

Tactic:
exact ⟨c, by simpa using hc.symm⟩

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (T R 0) = T R' 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case zero
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)
⊢ ((reflection hf * reflection hg) ^ 0) x =
    (Polynomial.eval t (S R 0) + Polynomial.eval t (S R (0 - 1))) • x + (Polynomial.eval t (S R (0 - 1)) * -g x) • y

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (U R 0) = U R' 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (C R 0) = C R' 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (S R 0) = S R' 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ derivative (T R 0) = ↑0 * U R (0 - 1)

Tactic:
| zero =>

Goal state after:
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
contra : g = 0
⊢ False

Tactic:
obtain ⟨n, hn, rfl⟩ : ∃ n : ι → ℕ, n ≠ 0 ∧ g = ∑ i, n i • b.baseSupp i := by
      simpa [hsV] using hg

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
n : ι → ℕ
hn : n ≠ 0
hg : ⇑(∑ i, n i • b.baseSupp i) ∈ sV
contra : ⇑(∑ i, n i • b.baseSupp i) = 0
⊢ False
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case zero
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
⊢ ↑(u ^ 0) = LinearMap.id + ↑0 • LinearMap.smulRight (f - g) x

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1.zero
ι : 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 : ι
h : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.reflection i) 0 = (P.reflection j) 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
⊢ (P.reflection j) 0 = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case zero
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
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[0] y = y + 0 • (f y • x - 2 • y)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case zero
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
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
⊢ (p (i x)) 0 = 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ (comap e.symm P).IsMaximal

Tactic:
apply Ring.DimensionLEOne.maximalOfPrime ?_ (P.comap_isPrime e.symm)

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ comap e.symm P ≠ ⊥
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ 2 * T R m * T R 0 = T R (m + 0) + T R (m - 0)

Tactic:
| zero =>

Goal state after:
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' = ⊤
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
hp : ∀ (i : ↑w) (j : ↑v), (bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b) i j ∈ (algebraMap K L).fieldRange
hA : ∀ (i : { x // x ∈ v }) (j : { x // x ∈ w }), b.toMatrix (⇑bM) i j ∈ (algebraMap K L).range
h_span : span K v = span K (Set.range ⇑b)
⊢ m ∈ span K (Set.range ⇑b)

Tactic:
Basis.mem_span_iff_repr_mem,

Goal state after:
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' = ⊤
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
hp : ∀ (i : ↑w) (j : ↑v), (bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b) i j ∈ (algebraMap K L).fieldRange
hA : ∀ (i : { x // x ∈ v }) (j : { x // x ∈ w }), b.toMatrix (⇑bM) i j ∈ (algebraMap K L).range
h_span : span K v = span K (Set.range ⇑b)
⊢ ∀ (i : { x // x ∈ v }), (b.repr m) i ∈ Set.range ⇑(algebraMap K L)
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:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 0 = C R (m + 0) + C R (m - 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (0 * n) = (T R 0).comp (T R n)

Tactic:
| zero =>

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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Tactic:
have h₁ := T_mul_T R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R (0 * n) = (C R 0).comp (C R n)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(s.toFun 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ StrictMono ⇑withZeroUnitsEquiv

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : WithZero αˣ
⊢ ∀ ⦃b : WithZero αˣ⦄, a < b → withZeroUnitsEquiv a < withZeroUnitsEquiv b
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsDomain R
inst✝ : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : (fun a ↦ n • a) a = (fun a ↦ n • a) b
⊢ a = b

Tactic:
simp only [nsmul_eq_mul, mul_eq_mul_left_iff, Nat.cast_eq_zero] at w

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsDomain R
inst✝ : CharZero R
n : ℕ
h : n ≠ 0
a b : R
w : a = b ∨ n = 0
⊢ a = b
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}
⊢ ∀ {a b : { N // N.FG }}, DvdNotUnit (f a) (f b) ↔ b < a

Tactic:
intro a

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}
a : { N // N.FG }
⊢ ∀ {b : { N // N.FG }}, DvdNotUnit (f a) (f b) ↔ b < a
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 ↑u⁻¹ ≤ 1

Tactic:
by
    rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]

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
⊢ ∀ (x y : K), Quotient.mk'' (x + y) ≤ max (Quotient.mk'' x) (Quotient.mk'' y)

Tactic:
intro a

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
a : K
⊢ ∀ (y : K), Quotient.mk'' (a + y) ≤ max (Quotient.mk'' a) (Quotient.mk'' y)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ ∀ (a b : R), ∃ c, a * c = b ∨ b * c = a

Tactic:
intro a

Goal state after:
case mpr
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a : R
⊢ ∀ (b : R), ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
⊢ ∀ ⦃a b : R⦄, ϖ = a * b → IsUnit a ∨ IsUnit b

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
a : R
⊢ ∀ ⦃b : R⦄, ϖ = a * b → IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ ∀ (a b : R), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
intro a

Goal state after:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
a : R
⊢ ∀ (b : R), p ∣ a * b → p ∣ a ∨ p ∣ b
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
x : M
hx : (of I M) x = u
n : ℕ
⊢ Submodule.Quotient.mk (f n) = (eval I M n) u

Tactic:
simp [u]

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

Goal state before:
pp: 𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ ∀ (a b : 𝒪), ∃ c, a * c = b ∨ b * c = a

Tactic:
intro a

Goal state after:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a : 𝒪
⊢ ∀ (b : 𝒪), ∃ c, a * c = b ∨ b * c = a