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

Goal state before:
pp: case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k : ℕ
hk : ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
⊢ ↑g (((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂)) = 0

Tactic:
hk,

Goal state after:
case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k : ℕ
hk : ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
⊢ ↑g 0 = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
    (fun i j ↦ Module.End.mapsTo_maxGenEigenspace_of_comm ?_) h'
  rcases eq_or_ne j i with rfl | hij <;> tauto

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
⊢ ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)

Tactic:
by
  induction n with
  | zero => simpa using hm
  | succ n IH =>
    simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
    rw [succ_nsmul, ← add_assoc, add_comm (n • _)]

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

Goal state before:
pp: 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
χ : R
x : L
m : M
⊢ m ∈ genWeightSpaceOf M χ x ↔ ∃ k, (((toEnd R L M) x - χ • 1) ^ k) m = 0

Tactic:
by
  simp [genWeightSpaceOf]

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

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ ∈ lowerCentralSeries R (↥H) (↥H) k
⊢ (H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0

Tactic:
hk,

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ ∈ ⊥
⊢ (H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
⊢ (Φ ↑y) ⁅↑x, z⁆ = 0

Tactic:
have hyz : ⁅(x : L), z⁆ ∈ I := lie_mem_left _ _ _ _ _ x.2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
hyz : ⁅↑x, z⁆ ∈ I
⊢ (Φ ↑y) ⁅↑x, z⁆ = 0
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ (Φ.restrict (LieIdeal.toLieSubalgebra K L I).toSubmodule).Nondegenerate

Tactic:
by
  rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]
  exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

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

Goal state before:
pp: case a
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
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅b, ↑I.incl y⁆ ∈ Submodule.map ↑I.incl ↑J

Tactic:
· suffices ⁅b, y.val⁆ = 0 by erw [this]; simp only [zero_mem]
          rw [← LieSubmodule.mem_bot (R := R) (L := L),
              ← (IsSemisimple.sSupIndep_isAtom hI).eq_bot]
          exact ⟨lie_mem_right R L I b y y.2, lie_mem_left _ _ _ _ _ hb⟩

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : m.ToType
⊢ 0 < count x.fst m

Tactic:
have := x.2.2; lia

Goal state after:
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 χ)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by
    nontriviality shiftedGenWeightSpace R L M χ
    apply Subtype.ext
    rw [coe_lie_shiftedGenWeightSpace_apply]
    simp only [smul_lie, LinearWeights.map_smul χ (aux R L M χ), smul_assoc t, SetLike.val_smul]
    rw [← smul_sub]
    congr

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
x : ↥m.toEnumFinset
⊢ (↑x).2 < count (↑x).1 m

Tactic:
by
      rw [← Multiset.mem_toEnumFinset]
      exact x.2

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
rw [h] at hf; cases hf

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case add
k : Type u
inst✝ : Field k
p✝ q✝ : MvPolynomial (Vars k) k
ha :
  ∀ (z : AlgebraicClosure k),
    (Ideal.Quotient.mk (maxIdeal k)) p✝ = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p✝)
hb :
  ∀ (z : AlgebraicClosure k),
    (Ideal.Quotient.mk (maxIdeal k)) q✝ = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) q✝)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝))

Tactic:
| add _ _ ha hb =>

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
hm : m ∈ Submodule.span R ↑S
⊢ (f ^ S.sup g) m = 0 m

Tactic:
induction hm using Submodule.span_induction with

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

Goal state before:
pp: case negSucc
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : -↑(chainBotCoeff α β) ≤ Int.negSucc n
hn' : Int.negSucc n ≤ ↑(chainTopCoeff α β)
⊢ genWeightSpace M (Int.negSucc n • α + ⇑β) ≠ ⊥

Tactic:
simp only [Int.negSucc_eq, ← Nat.cast_succ, neg_le_neg_iff, Nat.cast_le] at hn ⊢

Goal state after:
case negSucc
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn' : Int.negSucc n ≤ ↑(chainTopCoeff α β)
hn : n.succ ≤ chainBotCoeff α β
⊢ genWeightSpace M (-↑n.succ • α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : ↑S i ∈ ↑S '' Set.Iio m
⊢ ↑i < ↑m

Tactic:
Nat.cast_lt

Goal state after:
case h₁
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : ↑S i ∈ ↑S '' Set.Iio m
⊢ i < m
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✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : z ∈ ⁅⊤, ⊤⁆
⊢ 1 ⊗ₜ[R] z ∈ ⁅LieSubmodule.baseChange A ⊤, LieSubmodule.baseChange A ⊤⁆

Tactic:
← LieSubmodule.lie_baseChange

Goal state after:
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✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : z ∈ ⁅⊤, ⊤⁆
⊢ 1 ⊗ₜ[R] z ∈ LieSubmodule.baseChange A ⁅⊤, ⊤⁆
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-↑(k + 1) + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) -
      (2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1)) + T R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]; ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-↑(k + 1) + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) -
      (2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1)) + U R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]; ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-↑(k + 1) + 2) + (X * C R (-↑k) - C R (-↑k + 1)) -
      (X * C R (-↑(k + 1) + 1) - C R (-↑(k + 1)) + C R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]; ring_nf

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ S R (-↑(k + 1) + 2) + (X * S R (-↑k) - S R (-↑k + 1)) -
      (X * S R (-↑(k + 1) + 1) - S R (-↑(k + 1)) + S R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]; ring_nf

Goal state after:
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₁ • ⁅↑h, e⁆ + c₂ • ⁅↑h, f⁆ + c₃ • ⁅↑h, ⁅e, f⁆⁆ = (c₁ * α h) • e + (c₂ * -α h) • f + 0 • ⁅e, f⁆

Tactic:
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
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (C R n)) = eval ((algebraMap R R') x) (C R' n)

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]

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

Goal state before:
pp: case refine_2
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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N := f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF✝ : F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toPerfPair.symm F
hm : m = p.toPerfPair.symm F
y : M
m₀ : M'
hm' : i m₀ + y = m
n : N'
hy : (p y) (j n) = 0
⊢ ((p.compl₁₂ i j) m₀) n = f n

Tactic:
rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm] at hm'

Goal state after:
case refine_2
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
M' : Type u_4
N' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
i : M' →ₗ[R] M
j : N' →ₗ[R] N
hi : Injective ⇑i
hj : Injective ⇑j
hij : p.IsPerfectCompl i.range j.range
f : N' →ₗ[R] R
F : Dual R N := f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF✝ : F = f ∘ₗ linearProjOfIsCompl (Submodule.map (↑p.flip.toPerfPair.symm) i.range.dualAnnihilator) j hj ⋯
hF : ∀ (n : N'), F (j n) = f n
m : M := p.toPerfPair.symm F
hm : m = p.toPerfPair.symm F
y : M
m₀ : M'
hm' : p.toPerfPair (i m₀) + p.toPerfPair y = F
n : N'
hy : (p y) (j n) = 0
⊢ ((p.compl₁₂ i j) m₀) n = f n
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
⊢ IsPrecomplete ⊥ M

Tactic:
refine ⟨fun f hf => ⟨f 1, fun n => ?_⟩⟩

Goal state after:
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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f n ≡ f 1 [SMOD ⊥ ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case zero
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
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊥ ^ 0 • ⊤]

Tactic:
rw [pow_zero, Ideal.one_eq_top, top_smul]
    exact SModEq.top

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ v (x + y) = max (v x) (v y)

Tactic:
suffices ¬v (x + y) < max (v x) (v y) from
    or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ ¬v (x + y) < max (v x) (v y)
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
e : nilradical R = ⊤
⊢ False

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
I : Ideal R
hI : nilradical R < I
⊢ I = ⊤

Tactic:
· obtain ⟨n, hn⟩ := (Ideal.eq_top_iff_one _).mp e
      exact (H 0).mp .zero ((show (1 : R) = 0 by simpa using hn) ▸ isUnit_one)

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
I : Ideal R
hI : nilradical R < I
⊢ I = ⊤
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ 1 x ≤ 1

Tactic:
by
  rw [one_apply_def]
  split_ifs <;> simp_all

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ 1 x < 1 ↔ x = 0

Tactic:
by
  rw [one_apply_def]
  split_ifs <;> simp_all

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

Goal state before:
pp: case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
⊢ toWithBotNat 0 < toWithBotNat y

Tactic:
toWithBotNat_zero,

Goal state after:
case pos
R✝¹ : Type u
inst✝⁵ : CommRing R✝¹
inst✝⁴ : IsDomain R✝¹
inst✝³ : IsDiscreteValuationRing R✝¹
R✝ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
⊢ ⊥ < toWithBotNat y
Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : IsField R
⊢ IsIntegrallyClosed R

Tactic:
exact hf.toField.instIsIntegrallyClosed

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0' : a = 0
⊢ map (Ideal.Quotient.mk (comap C P)) m = map (Ideal.Quotient.mk (comap C P)) 0

Tactic:
by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0'

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

Tactic:
hk,

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