mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case smul
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
y : R
t : M
hy : t ∈ span R (range ⇑P.root)
hy' : t ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
⊢ y • t ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
| smul y t hy hy' =>

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
⊢ (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j) - (B.form (P.root i)) (P.root j)

Tactic:
← B.isOrthogonal_reflection j

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
i j : ι
⊢ (B.form ((P.reflection j) (P.root i))) ((P.reflection j) (P.root j)) =
    P.pairing i j * (B.form (P.root j)) (P.root j) - (B.form (P.root i)) (P.root j)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.hxy
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hx'.choose).2 * (ofClass v) (↑hy'.choose).1 ≠ 0

Tactic:
simpa only [MonoidWithZeroHom.coe_ofClass, ← map_mul v, ne_eq, h.eq_zero, map_mul w]
          using mul_ne_zero hx20 hy10

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x : (ofClass v).ValueGroup₀
⊢ h.orderMonoidIso x = (OrderMonoidIso.refl (ofClass v).ValueGroup₀) x

Tactic:
obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk

Goal state after:
case inl
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
⊢ h.orderMonoidIso 0 = (OrderMonoidIso.refl (ofClass v).ValueGroup₀) 0

case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x y : R
w✝¹ : (ofClass v) x ≠ 0
w✝ : (ofClass v) y ≠ 0
⊢ h.orderMonoidIso ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝) =
    (OrderMonoidIso.refl (ofClass v).ValueGroup₀) ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
x : (ofClass v).ValueGroup₀
⊢ (h.orderMonoidIso.trans h'.orderMonoidIso) x = ⋯.orderMonoidIso x

Tactic:
obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk

Goal state after:
case inl
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
⊢ (h.orderMonoidIso.trans h'.orderMonoidIso) 0 = ⋯.orderMonoidIso 0

case inr
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
x y : R
w✝¹ : (ofClass v) x ≠ 0
w✝ : (ofClass v) y ≠ 0
⊢ (h.orderMonoidIso.trans h'.orderMonoidIso) ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝) =
    ⋯.orderMonoidIso ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝)
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ (ρ.asAlgebraHom x) v ∈ p

Tactic:
apply x.induction_on <;> aesop

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

Goal state before:
pp: case weightMap
ι : 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
f g : P.End
hfg : (coweightHom P) f = (coweightHom P) g
x : M
⊢ f.weightMap x = g.weightMap x

Tactic:
dsimp [coweightHom] at hfg
    rw [MulOpposite.op_inj] at hfg
    have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M) (σ₂₃ := .id R) P.flip.toPerfPair) hfg
    rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h
    have : f.weightMap = g.weightMap := by
      have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
      refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))
    exact congrFun (congrArg DFunLike.coe this) x

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ (ρ (y * MulOpposite.unop z)) w = (ρ y) w

Tactic:
exact congr($(apply_eq_of_coe_eq ρ S _ _ (by simp_all)) w)

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
⊢ sInf s = ↑(b.leastOfBdd Hb Hinh)

Tactic:
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
  simp only [sInf, dif_pos this]
  convert! (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
b : ∀ i ∈ ∅, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ ∅, q ≤ ker (P.coroot' i)
⊢ q = ⊤

pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤

Tactic:
· replace c : q ≤ ⨅ i, LinearMap.ker (P.coroot' i) := by simpa using! c
    simp [h₀, ← P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'] at c

Goal state after:
case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case neg
ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∉ b.support
⊢ 0 i ≤ f i

Tactic:
replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi

Goal state after:
case neg
ι : 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
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∉ Function.support f
⊢ 0 i ≤ f i
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
i : ι
hi : -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
this : ∃ z, f (P.root (-i)) = ↑z
⊢ ∃ z, f (P.root i) = ↑z

Tactic:
by obtain ⟨z, hz⟩ := this; exact ⟨-z, by simp [← hz]⟩

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
⊢ False

Tactic:
have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _))

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1' : a1 ≤ abv (↑f i)
⊢ False
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j

pp: case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j

Tactic:
· rwa [abs_of_nonneg] at this
    rw [abs_of_nonneg h] at h₁
    exact
      (le_add_iff_nonneg_right _).1
        (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)

Goal state after:
case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑(-f) j
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0

Tactic:
dif_pos

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ 0 = const abv 0

case hc
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (const abv 0).LimZero
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m

Tactic:
induction n generalizing m with
  | zero => simp
  | succ n IH =>
    rcases m with m | m
    · simp
    rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
    · calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
    · simp [h]

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

Goal state before:
pp: case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit (A ^ (↑z + 1)).det ↔ IsUnit A.det ∨ ↑z + 1 = 0

Tactic:
rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
      Int.ofNat_inj]

Goal state after:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ Q ≤ q

Tactic:
rw [Q_def, q_def, ← mulVec_mulVec, dotProduct_mulVec, dotProduct, Finset.mul_sum]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ ∑ i, μ * (d i * |v i| ^ 2) ≤ ∑ i, (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
⊢ (minpoly R f).IsRoot μ

Tactic:
by
  rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩
  refine Or.resolve_right (smul_eq_zero.1 ?_) ne0
  rw [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩]
  simp

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
⊢ b.h' i ∈ corootSpace ⇑(Weight.toLinear K (↥H) L ↑(b.baseSupp' i))

Tactic:
h_eq

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
⊢ ⟨⁅b.e i, b.f i⁆, h_mem⟩ ∈ corootSpace ⇑(Weight.toLinear K (↥H) L ↑(b.baseSupp' i))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ X + 1 = map (algebraMap ℕ R) (X + 1)

Tactic:
simp only [Polynomial.map_add, map_X,
      Polynomial.map_one]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * ↑0 = ↑((n - k) * 0)

Tactic:
Nat.cast_zero,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * 0 = ↑((n - k) * 0)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodH eι b₁ b₂ i ∈ ↑(lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))

Tactic:
hef

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ ∈
    ↑(lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
⊢ prod eι b₁ b₂ < ⊤

Tactic:
have := Fintype.ofFinite ι₁
  have := Fintype.ofFinite ι₂
  have := b₁.isCartanSubalgebra
  have := b₂.isCartanSubalgebra
  have := (basisProd eι b₁ b₂ hA).isCartanSubalgebra
  rw [lt_top_iff_ne_top]
  intro contra
  have (x : H₁ × H₂) (hx) : ⟨(x.1, x.2), hx⟩ ∈ prodCartan eι b₁ b₂ := by
    rw [← mem_toLieSubmodule, ← rootSpace_zero_eq, LieModule.mem_genWeightSpace]
    refine fun ⟨y, hy⟩ ↦ ⟨1, ?_⟩
    simpa [Subtype.ext_iff] using ⟨lie_fst_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.fst,
      lie_snd_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.snd⟩
  let f : H₁ × H₂ →ₗ[K] prodCartan eι b₁ b₂ :=
    { toFun x := ⟨⟨⟨x.fst, x.snd⟩, by simp [contra]⟩, this x _⟩
      map_add' := by simp
      map_smul' := by simp }
  have f_inj : Injective f := fun x y h ↦ by simpa [Prod.ext_iff, f] using h
  let g : H₁ × H₂ →ₗ[K] H₁ := (prodCartanEquiv eι b₁ b₂) ∘ₗ f
  have hg₁ : Injective g := by simpa [g]
  obtain ⟨x₂ : H₂, hx₂ : x₂ ≠ 0⟩ := exists_ne (0 : H₂)
  have hg₂ : g (0, x₂) = g (0, 0) := rfl
  aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
⊢ (b.toMatrix ⇑b' * (toMatrix b' b') f * b'.toMatrix ⇑b).charpoly = ((toMatrix b' b') f).charpoly

Tactic:
set P := b.toMatrix b'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
⊢ (P * (toMatrix b' b') f * b'.toMatrix ⇑b).charpoly = ((toMatrix b' b') f).charpoly