mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
t : R
x : L
⊢ χ (t • x) = t • χ x

Tactic:
simp_rw [Ne, ← LieSubmodule.toSubmodule_inj, genWeightSpace, genWeightSpaceOf,
        LieSubmodule.iInf_toSubmodule, LieSubmodule.bot_toSubmodule] at hχ
      exact Module.End.map_smul_of_iInf_genEigenspace_ne_bot
        (toEnd R L M).toLinearMap χ _ hχ t x

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' = ⊥
⊢ J = ⊥

Tactic:
rw [eq_bot_iff] at this ⊢

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' ≤ ⊥
⊢ J ≤ ⊥
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅t • x, m⁆ = ↑(t • ⁅x, m⁆)

Tactic:
rw [coe_lie_shiftedGenWeightSpace_apply]

Goal state after:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, ↑m⁆ - χ (t • x) • ↑m = ↑(t • ⁅x, m⁆)
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅x, t • m⁆ = ↑(t • ⁅x, m⁆)

Tactic:
rw [coe_lie_shiftedGenWeightSpace_apply]

Goal state after:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, ↑(t • m)⁆ - χ x • ↑(t • m) = ↑(t • ⁅x, m⁆)
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Tactic:
apply (mul_divByMonic_eq_iff_isRoot
    (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr

Goal state after:
K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
a : f.SplittingField
ha : a ≠ 0
⊢ e (a * e.symm (e a)⁻¹) = e 1

Tactic:
by simp [EmbeddingLike.map_ne_zero_iff.2 ha]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
⊢ Injective f

Tactic:
intro k

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
k : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄, f k = f a₂ → k = a₂
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case mem
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ ((traceForm R L M) a) c = 0

Tactic:
h,

Goal state after:
case mem
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : ⁅φ b, y⁆ = -φ c
⊢ (0 a) c = 0
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
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-⇑α) x✝ = 0 x✝

Tactic:
h,

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
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-0) x✝ = 0 x✝
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : LieRing.IsNilpotent L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsTorsionFree R M
inst✝¹ : IsNoetherian R M
inst✝ : IsTriangularizable R L M
z : L
⊢ traceForm R L M = ∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf M χ z)

Tactic:
ext x y
  have hxy : ∀ χ : R, MapsTo ((toEnd R L M x).comp (toEnd R L M y))
      (genWeightSpaceOf M χ z) (genWeightSpaceOf M χ z) :=
    fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
  have hfin : {χ : R | (genWeightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
    simp_rw [ne_eq, LieSubmodule.toSubmodule_eq_bot (genWeightSpaceOf M _ _)]
    exact finite_genWeightSpaceOf_ne_bot R L M z
  classical
  have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]
  simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
  exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)

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
h : f x = 2
⊢ x - f x • x = -x

Tactic:
h,

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
h : f x = 2
⊢ x - 2 • x = -x
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
hyp : coroot α = coroot β
hα : β.IsZero
⊢ α.IsZero

Tactic:
simp only [← coroot_eq_zero_iff] at hα ⊢

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
hyp : coroot α = coroot β
hα : coroot β = 0
⊢ coroot α = 0
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
hyp : coroot α = coroot β
hα : ¬α.IsZero
hβ : β.IsNonZero
this✝ : Weight.ker = Weight.ker
this : Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
⊢ α = β

Tactic:
by ext x; simpa using LinearMap.congr_fun this x

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

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

Tactic:
sub_comp,

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ (X * C R (↑n + 1)).comp (2 * X) - (C R ↑n).comp (2 * X) = 2 * (2 * X * T R (↑n + 1) - T R ↑n)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
sub_comp,

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ (X * C R (-↑n)).comp (2 * X) - (C R (-↑n + 1)).comp (2 * X) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 1))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
sub_comp,

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ (X * S R (↑n + 1)).comp (2 * X) - (S R ↑n).comp (2 * X) = 2 * X * U R (↑n + 1) - U R ↑n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (-↑n)).comp (2 * X) = U R (-↑n)
ih2 : (S R (-↑n + 1)).comp (2 * X) = U R (-↑n + 1)
⊢ (X * S R (-↑n) - S R (-↑n + 1)).comp (2 * X) = 2 * X * U R (-↑n) - U R (-↑n + 1)

Tactic:
sub_comp,

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (-↑n)).comp (2 * X) = U R (-↑n)
ih2 : (S R (-↑n + 1)).comp (2 * X) = U R (-↑n + 1)
⊢ (X * S R (-↑n)).comp (2 * X) - (S R (-↑n + 1)).comp (2 * X) = 2 * X * U R (-↑n) - U R (-↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : S R ↑n ^ 2 + S R (↑n + 1) ^ 2 - X * S R ↑n * S R (↑n + 1) = 1
h₁ : S R (↑n + 2) = X * S R (↑n + 1) - S R ↑n
⊢ S R (↑n + 1) ^ 2 + S R (↑n + 1 + 1) ^ 2 - X * S R (↑n + 1) * S R (↑n + 1 + 1) = 1

Tactic:
linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (T R n) = eval x (T R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_T]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (⇑derivative)^[0] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - 0))

Tactic:
rw [Function.iterate_zero_apply]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ T R ↑n ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - 0))
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 : ι
h : P.IsOrthogonal i j
x✝ : M
⊢ P.pairing i j = 0 ∧ P.pairing j i = 0

Tactic:
simpa [IsOrthogonal] using h

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Tactic:
simp_rw [← B.transpose_apply] at h_mem

Goal state after:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), Bᵀ j i ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K
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
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
⊢ ∀ (k : ι), (c i) (r k) = (c j) (r k)

Tactic:
intro k

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
k : ι
⊢ (c i) (r k) = (c j) (r k)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ x = mk' K (num A y) (den A y)

Tactic:
h,

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A y) (den A y)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A x) (den A x)

Tactic:
h,

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A y) (den A y)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : num A x = 0
⊢ 0 = (algebraMap A K) (num A x)

Tactic:
h,

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : num A x = 0
⊢ 0 = (algebraMap A K) 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have h₁ := C_mul_C R ((m + 1) * n) n

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀ˣ
⊢ embedding ((restrict₀ f) 0) < embedding ↑a

Tactic:
embedding_strictMono.lt_iff_lt

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : f.ValueGroup₀ˣ
⊢ (restrict₀ f) 0 < ↑a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mpr
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
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
⊢ Nontrivial O

Tactic:
obtain ⟨o1, ho1⟩ := hv.exists_of_le_one (r := 1) (by simp)

Goal state after:
case mpr
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
h : Nontrivial R
o0 : O
ho0 : (algebraMap O R) o0 = 0
o1 : O
ho1 : (algebraMap O R) o1 = 1
⊢ Nontrivial O
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
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ v ((algebraMap O F) y) < v ((algebraMap O F) x)

Tactic:
rw [lt_iff_le_not_ge, hv.le_iff_dvd, hv.le_iff_dvd]

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x
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
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = (lift I f) ((of I M) x)

Tactic:
lift_of,

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
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = f x
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
⊢ v ((algebraMap (↥v.integer) K) y) ≤ min 1 γ

Tactic:
rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩

Goal state after:
case mp.inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = 1
right✝ : 1 ≤ γ
⊢ v ((algebraMap (↥v.integer) K) y) ≤ min 1 γ

case mp.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
y : ↥v.integer
hy : v ↑y ≤ γ
h : min 1 γ = γ
right✝ : γ < 1
⊢ v ((algebraMap (↥v.integer) K) y) ≤ min 1 γ
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
hab : ϖ = a * b
ha : a ∈ maximalIdeal R
hb : b ∈ maximalIdeal R
⊢ False

Tactic:
h,

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 b : R
hab : ϖ = a * b
ha : a ∈ span {ϖ}
hb : b ∈ span {ϖ}
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ maximalIdeal R = ⊥

Tactic:
h,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ span {ϖ} = ⊥
Module: Mathlib.RingTheory.Jacobson.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
this : f.coeff n ∈ ⊥.jacobson
⊢ f.coeff n = 0

Tactic:
h,

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
this : f.coeff n ∈ ⊥
⊢ f.coeff n = 0
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ Antitone fun n ↦ I ^ a n • ⊤

pp: case refine_2
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ ∀ (m : ℕ), (f m) x = (Submodule.factor ⋯) ((f (m + 1)) x)

Tactic:
· exact fun _ _ le ↦ smul_mono_left (Ideal.pow_le_pow_right (ha.monotone le))

Goal state after:
case refine_2
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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
x : M
⊢ ∀ (m : ℕ), (f m) x = (Submodule.factor ⋯) ((f (m + 1)) x)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ↑u * p ^ m * ↑v⁻¹ = q ^ n

Tactic:
h,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ↑v * q ^ n * ↑v⁻¹ = q ^ n