mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ Submodule.Quotient.mk ((ofLinearEquiv I N).symm ((AdicCompletion.lift I f ⋯) x)) = (f n) x

Tactic:
← mkQ_apply,

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
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ (I ^ n • ⊤).mkQ ((ofLinearEquiv I N).symm ((AdicCompletion.lift I f ⋯) x)) = (f n) 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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x : M
⊢ Submodule.Quotient.mk ((LinearEquiv.ofBijective (of I N) ⋯).symm ((AdicCompletion.lift I (extend ha f) ⋯) x)) =
    (f n) x

Tactic:
← mkQ_apply,

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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x : M
⊢ (I ^ a n • ⊤).mkQ ((LinearEquiv.ofBijective (of I N) ⋯).symm ((AdicCompletion.lift I (extend ha f) ⋯) x)) = (f n) x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Irreducible x✝

Tactic:
apply hfx.1

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ x✝ ∈ fx
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intro p1 p2 h1 h2

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
p p1 p2 : R[X]
h1 : p1 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
h2 : p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ p1 + p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Tactic:
simp only [← one_lt_val_iff v h, le_or_gt]

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

Goal state before:
pp: R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
n : ℕ∞ᵒᵈ
⊢ (fun I ↦ OrderDual.toDual ((addVal R) (generator I)))
      ((fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n)) n) =
    n

Tactic:
obtain ⟨k, rfl⟩ := OrderDual.toDual.surjective n
    dsimp
    induction k with
    | top => simp
    | coe k =>
      obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
      rw [OrderDual.toDual_inj, ENat.recTopCoe_natCast, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]
      exact associated_generator_span_self (ϖ ^ k)

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (addVal R) x ≤ (addVal R) y ↔ x ∣ y

Tactic:
generalize hvx : addVal R x = vx

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ∞
hvx : (addVal R) x = vx
⊢ vx ≤ (addVal R) y ↔ x ∣ y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg
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✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
H : ¬(v x ≠ 0 ∨ v y ≠ 0)
⊢ (↑(restrict₀ (ofClass v))).toFun (x + y) ≤
    max ((↑(restrict₀ (ofClass v))).toFun x) ((↑(restrict₀ (ofClass v))).toFun y)

Tactic:
· simp only [ne_eq, not_or, Decidable.not_not] at H
      simp only [ZeroHom.toFun_eq_coe, toZeroHom_coe, restrict₀_apply,
        MonoidWithZeroHom.coe_ofClass, H, ↓reduceDIte, max_self, nonpos_iff_eq_zero]
      replace H : v (x + y) = 0 :=
        le_antisymm (map_add_le _ (le_of_eq H.1) (le_of_eq H.2)) zero_le
      simp [H]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
isloc : IsLocalization M' (Localization M')
⊢ (IsLocalization.map (Localization M') φ ⋯).IsIntegral

Tactic:
exact @isIntegral_isLocalization_polynomial_quotient R _
          (Localization M) (Localization M') _ _ P pX hpX _ _ _ isloc

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

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
⊢ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) = ↑(⨅ i, LinearMap.ker (P.root' i))

Tactic:
by ext; simp [LinearEquiv.symm_apply_eq, subset_def]

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

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
⊢ ↑(Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator) =
    ↑(span R (range P.root')).dualCoannihilator

Tactic:
by ext; simp [LinearEquiv.symm_apply_eq, subset_def]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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
inst✝ : Fintype ι
i : ι
⊢ ((P.RootFormIn R) (P.rootSpanMem R i)) (P.rootSpanMem R i) • P.coroot i = 2 • P.Polarization (P.root i)

Tactic:
P.rootFormIn_self_smul_coroot R i,

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
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
⊢ 2 • (P.PolarizationIn R) (P.rootSpanMem R i) = 2 • P.Polarization (P.root i)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan R, (P.RootForm n) x = 0
⊢ ∃ u ∈ P.rootSpan R, ∃ v ∈ LinearMap.ker P.RootForm, u + v = y

Tactic:
by
    rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : LinearOrder S
inst✝⁶ : IsStrictOrderedRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : ↥(span S (range ⇑P.root))
s : S
left✝ : s ≥ 0
hs : (algebraMap S R) s = (P.RootForm ↑x) ↑x
this : s = ((P.posRootForm S).posForm x) x
⊢ 0 ≤ ((P.posRootForm S).posForm x) x

Tactic:
rwa [← this]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ ∑ i, (Q i) ((x + y) i) - ∑ i, (Q i) (x i) - ∑ i, (Q i) (y i) =
    ∑ x_1, (Q x_1) (x x_1 + y x_1) - ∑ i, (Q i) (x i) - ∑ i, (Q i) (y i)

Tactic:
Pi.add_apply

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

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
hα : ¬α.IsZero
⊢ genWeightSpace L (-(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) ≠ ⊥

Tactic:
rootSpace_zsmul_add_ne_bot_iff α β hα

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α β : Weight K (↥H) L
hα : ¬α.IsZero
⊢ -(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)) ≤ ↑(chainTopCoeff (⇑α) β) ∧
    - -(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)) ≤ ↑(chainBotCoeff (⇑α) β)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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 : f.coweightMap = g.coweightMap
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
set y := f.indexEquiv x with hy

Goal state after:
case indexEquiv
ι : 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 : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
⊢ y = g.indexEquiv x
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ (rootSystem H).flip.RootForm =
    ∑ α ∈ LieSubalgebra.root, (Weight.toLinear K (↥H) L α).smulRight (Weight.toLinear K (↥H) L α)

Tactic:
← Finset.sum_coe_sort (s := H.root)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ (rootSystem H).flip.RootForm = ∑ i, (Weight.toLinear K (↥H) L ↑i).smulRight (Weight.toLinear K (↥H) L ↑i)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝⁷ : AddCommGroup M₂✝
inst✝⁶ : Module R M₂✝
inst✝⁵ : AddCommGroup N₂✝
inst✝⁴ : Module R N₂✝
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂✝ R M₂✝ N₂✝
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ ⇑↑(weightEquiv P Q f).symm ∘ ⇑Q.root = ⇑P.root ∘ ⇑(↑f).indexEquiv.symm

Tactic:
ext i
    simp only [LinearEquiv.coe_coe, comp_apply]
    have := f.root_weightMap
    rw [funext_iff] at this
    specialize this (f.indexEquiv.symm i)
    simp only [comp_apply, Equiv.apply_symm_apply] at this
    simp [← this]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.single
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
h : α
y : k[G]
⊢ MonoidAlgebra.single g a • Finsupp.single h y =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h y)

Tactic:
induction y using MonoidAlgebra.induction_linear with

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

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
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : ↑(MulOpposite.unop ((coweightHom P) g)) = ↑(MulOpposite.unop ((coweightHom P) g'))
⊢ g = g'

Tactic:
coweightHom_toLinearMap,

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
P : RootPairing ι R M N
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = ↑(MulOpposite.unop ((coweightHom P) g'))
⊢ g = g'
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz : (fun z ↦ Exists.choose ⋯) ⟨z, hz⟩ = (fun z ↦ Exists.choose ⋯) ⟨z', hz'⟩
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
⊢ P.root (Exists.choose hz) = P.root (Exists.choose hz')

Tactic:
P.root.injective.eq_iff

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz : (fun z ↦ Exists.choose ⋯) ⟨z, hz⟩ = (fun z ↦ Exists.choose ⋯) ⟨z', hz'⟩
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
⊢ Exists.choose hz = Exists.choose hz'
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairing i j = 0 ∧ P.pairing i j = 0
⊢ P.pairingIn ℤ i j = 0

Tactic:
and_self,

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
P : RootPairing ι R M N
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairing i j = 0
⊢ P.pairingIn ℤ i j = 0
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:
obtain ⟨z, hz⟩ := this; exact ⟨-z, by simp [← hz]⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
⊢ P.root (chainTopIdx i j) = P.root j + chainTopCoeff i j • P.root i

Tactic:
by_cases h : LinearIndependent R ![P.root i, P.root j]
  · simp only [chainTopIdx, reduceDIte, h]
    exact (P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h).mpr
      (le_refl <| P.chainTopCoeff i j) |>.choose_spec
  · simp only [chainTopIdx, chainTopCoeff, h, reduceDIte, zero_smul, add_zero]

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

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
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
heq : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ b.height i = ∑ j ∈ b.support, f j

Tactic:
suffices ∀ j ∈ b.support, (b.exists_root_eq_sum_int i).choose j = f j from
    Finset.sum_congr rfl this

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
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
heq : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∀ j ∈ b.support, ⋯.choose j = f j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case pos
ι : 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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ i ∈ b.support, 0 ≤ f i
j : ι
hj : j ∈ Function.support f
⊢ f j = 0

Tactic:
exact le_antisymm (neg.le j) (contra j (hf₀ hj))

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

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
b : P.Base
inst✝ : CharZero R
i j k : ι
hk : P.root k = P.root i + P.root j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
hfg : P.root k = ∑ l ∈ b.support, (f + g) l • P.root l
⊢ ∑ j ∈ b.support, (f + g) j = ∑ x ∈ b.support, (f x + g x)

Tactic:
Pi.add_apply

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ ↑(chainBotCoeff i (chainTopIdx i j)) - ↑(chainTopCoeff i (chainTopIdx i j)) = P.pairingIn ℤ (chainTopIdx i j) i

Tactic:
P.chainBotCoeff_sub_chainTopCoeff h

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ P.pairingIn ℤ (chainTopIdx i j) i = P.pairingIn ℤ (chainTopIdx i j) i
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ ↑(chainBotCoeff i j) + ↑(chainTopCoeff i j) = P.pairingIn ℤ (chainTopIdx i j) i

Tactic:
calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]

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

Goal state before:
pp: R₁ : Type u_1
M₁ : Type u_2
inst✝⁸ : CommSemiring R₁
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
n : Type u_5
o : Type u_6
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₁ M₁
M₂' : Type u_7
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₁ M₂'
c : Basis o R₁ M₂'
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ ((toBilin b) M).comp ((toLin c b) P) ((toLin c b) Q) = (toBilin c) (Pᵀ * M * Q)

Tactic:
ext x y
  rw [Matrix.toBilin, LinearMap.BilinForm.toMatrix, Matrix.toBilin, LinearMap.BilinForm.toMatrix,
    toMatrix₂_symm, toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]
  simp

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
⊢ False

Tactic:
by
  have hlz : LimZero (f * g) := by simpa
  have hf' : ¬LimZero f := by simpa using show ¬LimZero (f - 0) from hf
  have hg' : ¬LimZero g := by simpa using show ¬LimZero (g - 0) from hg
  rcases abv_pos_of_not_limZero hf' with ⟨a1, ha1, N1, hN1⟩
  rcases abv_pos_of_not_limZero hg' with ⟨a2, ha2, N2, hN2⟩
  have : 0 < a1 * a2 := mul_pos ha1 ha2
  obtain ⟨N, hN⟩ := hlz _ this
  let i := max N (max N1 N2)
  have hN' := hN i (le_max_left _ _)
  have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _))
  have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _))
  apply not_le_of_gt hN'
  change _ ≤ abv (_ * _)
  rw [abv_mul abv]
  gcongr

Goal state after: