mathlib-initiative/mathlib-tactics huggingface dataset:
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
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    ∑ i ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥↑(genWeightSpace M (i • α + χ))) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)

Tactic:
simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]

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
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : 0 < ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
h₁ : iSupIndep fun i ↦ (fun k ↦ ↑(genWeightSpace M (k • α + χ))) ↑i
h₂ :
  ∀ (i : ℤ),
    MapsTo ⇑((toEnd R (↥H) M) x) ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
      ↑((fun k ↦ ↑(genWeightSpace M (k • α + χ))) i)
h₃ : ↑(genWeightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, (fun k ↦ ↑(genWeightSpace M (k • α + χ))) i
⊢ ((∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i) • α +
        ↑(∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))) • χ)
      x =
    ∑ x_1 ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥↑(genWeightSpace M (x_1 • α + χ))) ((toEnd R ↥H ↥(genWeightSpace M (x_1 • α + χ))) x)
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: case neg
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 : n < (chainTopCoeff α β).succ
hα : ¬α = 0
⊢ genWeightSpace M (n • α + ⇑β) ≠ ⊥

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case neg
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 : n < chainTopCoeff α β + 1
hα : ¬α = 0
⊢ genWeightSpace M (n • α + ⇑β) ≠ ⊥
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case zero
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
x y : L
hx : x ∈ ⊤.lcs L 0
hy : y ∈ LieSubmodule.ucs 0 ⊥
⊢ ((traceForm R L M) x) y = 0

Tactic:
replace hy : y = 0 := by simpa using hy
    simp [hy]

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

Goal state before:
pp: 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
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
← trans_dualMap_symm_flip e

Goal state after:
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
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Bijective ⇑↑(e ≪≫ₗ e.flip.symm.dualMap)
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: 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
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ (map (↑e ∘ₗ ↑e.symm) p).dualCoannihilator = map (↑e.flip.symm ∘ₗ ↑e.flip) p.dualCoannihilator

Tactic:
simp [-coe_toLinearMap_flip]

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
⊢ ⊤ ≤ ⊥.dualAnnihilator

Tactic:
Submodule.dualAnnihilator_bot

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
⊢ ⊤ ≤ ⊤
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
⊢ ⨆ i, Weight.ker.dualAnnihilator = ⊥.dualAnnihilator

Tactic:
Submodule.dualAnnihilator_bot

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
⊢ ⨆ i, Weight.ker.dualAnnihilator = ⊤
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 x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ (trace A (A ⊗[R] M)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) = 0

Tactic:
apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero

Goal state after:
case hf
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 x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ ⨆ μ, ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace μ = ⊤

case hg
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 x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ ∀ (μ : A),
    (trace A ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace μ))
        (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) =
      0

case h_comm
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 x : L
A : Type u_1 := ⋯
hz : 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1
hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L)
⊢ Commute ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z))
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✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ =
    (((traceForm R L M).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule) ⟨x, hx⟩) ⟨y, hy⟩

Tactic:
change _ = trace R M (φ x ∘ₗ φ y)

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✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ((traceForm R ↥I ↥N) ⟨x, hx⟩) ⟨y, hy⟩ = (trace R M) (φ x ∘ₗ φ y)
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_1
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α : ¬α.IsZero
x : ↥H
hx : x ∈ (traceForm K (↥H) L).orthogonal (K ∙ coroot α)
⊢ x ∈ Weight.ker

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α : ¬α.IsZero
x : ↥H
hx : x ∈ Weight.ker
y : ↥H
hy : y ∈ K ∙ coroot α
⊢ ((traceForm K (↥H) L) y) x = 0

Tactic:
· simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
      specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
      simp only [traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
      simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)

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α : ¬α.IsZero
x : ↥H
hx : x ∈ Weight.ker
y : ↥H
hy : y ∈ K ∙ coroot α
⊢ ((traceForm K (↥H) L) y) x = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem
ι : 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
x : L
i : ι
⊢ ∀ (a : L) (b_1 : a ∈ H),
    ∃ k, (((LieModule.toEnd R L L) a - (∑ x, ↑(Pi.single i 1 x) * (b.baseSupp x) ⟨a, b_1⟩) • 1) ^ k) (b.e i) = 0

Tactic:
exact fun y hy ↦ ⟨1, by simp [Pi.single_apply]⟩

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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
⊢ (∃ c₁ c₂ c₃,
      x = c₁ • Classical.choose he + c₂ • Classical.choose hf + c₃ • ⁅Classical.choose he, Classical.choose hf⁆) ↔
    ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
have hcf₀ : cf ≠ 0 := by
    rintro rfl
    simp only [zero_smul] at hcf
    exact he.choose_spec.choose_spec.1.f_ne_zero hcf

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
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H ⇑α
htf : f ∈ rootSpace H (-⇑α)
x : L
pf✝² : LieRing.IsNilpotent ↥H
pf✝¹ : LieModule K (↥H) L
pf✝ : ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
he : ∃ e f, IsSl2Triple (Classical.choose pf✝) e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
hf :
  ∃ f,
    IsSl2Triple (Classical.choose pf✝) (Classical.choose he) f ∧
      Classical.choose he ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
ce : K
hce : he.choose = ce • e
cf : K
hcf : hf.choose = cf • f
hce₀ : ce ≠ 0
hcf₀ : cf ≠ 0
⊢ (∃ c₁ c₂ c₃,
      x = c₁ • Classical.choose he + c₂ • Classical.choose hf + c₃ • ⁅Classical.choose he, Classical.choose hf⁆) ↔
    ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2

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
y : M
g : Dual R M
inst✝ : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
⊢ x = y

Tactic:
suffices h : f y • x = (2 : R) • y by
    rw [hfy, two_smul R x, two_smul R y, ← two_zsmul, ← two_zsmul] at h
    exact smul_right_injective _ two_ne_zero h
  contrapose! hΦ
  apply ((infinite_range_reflection_reflection_iterate_iff hfx hgy
    (by rw [hfy, hgx]; norm_cast)).mpr hΦ).mono
  rw [range_subset_iff]
  intro n
  rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo hfx hxfΦ).comp
    (bijOn_reflection_of_mapsTo hgy hygΦ)).image_eq n]
  exact mem_image_of_mem _ hyΦ

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
⊢ ∃ a, (p.compl₁₂ i j) a = f

Tactic:
· set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF
    have hF (n : N') : F (j n) = f n := by simp [hF]
    set m : M := p.toPerfPair.symm F with hm
    obtain ⟨-, y, ⟨m₀, rfl⟩, hy, hm'⟩ :=
      Submodule.codisjoint_iff_exists_add_eq.mp hij.isCompl_left.codisjoint m
    refine ⟨m₀, LinearMap.ext fun n ↦ ?_⟩
    replace hy : (p y) (j n) = 0 := by
      simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy
      obtain ⟨g, hg, rfl⟩ := hy
      simpa using hg _ (LinearMap.mem_range_self j n)
    rw [hm, ← LinearEquiv.symm_apply_eq, map_add, LinearEquiv.symm_symm] at hm'
    simpa [← hF, ← LinearMap.congr_fun hm' (j n)]

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' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
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'
this : span K (Set.range v') = ⊤
e : { x // x ∈ v } ≃ Fin (Nat.card { x // x ∈ v }) := Finite.equivFin { x // x ∈ v }
b' : Basis (↑v) K ↥M' := Basis.mk hv' ⋯
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : FiniteDimensionalOrder (Submodule R M)
⊢ (WellFounded fun x1 x2 ↦ x1 > x2) ∧ IsArtinian R M

Tactic:
isArtinian_iff

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : FiniteDimensionalOrder (Submodule R M)
⊢ (WellFounded fun x1 x2 ↦ x1 > x2) ∧ WellFounded fun x1 x2 ↦ x1 < x2
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
⊢ length R M = length R N + length R P

Tactic:
by
  by_cases hP : IsFiniteLength R P
  · by_cases hN : IsFiniteLength R N
    · obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP
      obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN
      let s' : CompositionSeries (Submodule R M) :=
        s.map ⟨Submodule.comap g, Submodule.comap_covBy_of_surjective hg⟩
      let t' : CompositionSeries (Submodule R M) :=
        t.map ⟨Submodule.map f, Submodule.map_covBy_of_injective hf⟩
      have hfg : Submodule.map f ⊤ = Submodule.comap g ⊥ := by
        rw [Submodule.map_top, Submodule.comap_bot, LinearMap.exact_iff.mp H]
      let r := t'.smash s' (by simpa [s', t', hs₁, ht₂] using hfg)
      rw [← Module.length_compositionSeries s hs₁ hs₂,
        ← Module.length_compositionSeries t ht₁ ht₂,
        ← Module.length_compositionSeries r
          (by simpa [r, t', ht₁, -Submodule.map_bot] using Submodule.map_bot f)
          (by simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g)]
      simp_rw [r, RelSeries.smash_length, Nat.cast_add, s', t', RelSeries.map_length]
    · have := mt (IsFiniteLength.of_injective · hf) hN
      rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
      rw [hN, this, top_add]
  · have := mt (IsFiniteLength.of_surjective · hg) hP
    rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
    rw [hP, this, add_top]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b✝ : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
left✝ : IsNoetherian R R
right✝ : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ length R M = Cardinal.toENat (Module.rank R M) * length R R

Tactic:
rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]

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
⊢ ∀ (a : ValueGroup A K), 0 * a = 0

Tactic:
rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]

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

Goal state before:
pp: case mk.mk.mk
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✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
hbc : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
⊢ ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤
      Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b

Tactic:
contrapose hbc

Goal state after:
case mk.mk.mk
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✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
c : K
hbc :
  Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤
    Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a * Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
⊢ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) c ≤ Quot.mk (⇑(MulAction.orbitRel Aˣ K)) b
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: 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)

Tactic:
· intro y hy
      simp only [Function.comp_apply, hx, Ideal.submodule_span_eq, Set.mem_image,
        SetLike.mem_coe, Ideal.mem_span_singleton] at hy
      obtain ⟨y, hy, rfl⟩ := hy
      exact le_of_dvd hv hy

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

Goal state before:
pp: case mp
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
⊢ ValuationRing R → ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
intro H x
    obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x
    have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
    obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
    · exact Or.inr
        ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩
    · exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩

Goal state after: