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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
x✝ : ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y
s : S
h : s > 0
h' : (algebraMap S R) s = (algebraMap S R) ((B.posForm x) y)
⊢ 0 < (B.posForm x) y

Tactic:
rwa [← FaithfulSMul.algebraMap_injective S R h']

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)
⊢ 2 - (p (root i)) (coroot j) * (p (root j)) (coroot i) + (p (root j)) (coroot i) * (p (root i)) (coroot j) = 2

Tactic:
rw [mul_comm (p (root i) (coroot j))]

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)
⊢ 2 - (p (root j)) (coroot i) * (p (root i)) (coroot j) + (p (root j)) (coroot i) * (p (root i)) (coroot j) = 2
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 j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
⊢ 4 • (P.RootForm (P.root i)) (P.root j) ^ 2 =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
have hji : 2 • (P.RootForm (P.root i)) (P.root j) =
      P.toLinearMap (P.root i) (2 • P.Polarization (P.root j)) := by
    rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]

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 j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ 4 • (P.RootForm (P.root i)) (P.root j) ^ 2 =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

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✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
⊢ n • P.root i ∉ range ⇑P.root

Tactic:
by
  have : ¬ LinearIndependent R ![n • P.root i, P.root i] := by
    simpa only [LinearIndependent.pair_iff, not_forall] using
      ⟨1, -(n : R), by simp [Nat.cast_smul_eq_nsmul], by simp⟩
  rintro ⟨j, hj⟩
  replace this : j = i ∨ P.root j = -P.root i := by
    simpa only [← hj, IsReduced.linearIndependent_iff, not_and_or, not_not] using this
  rcases this with rfl | this
  · replace hj : (1 : ℤ) • P.root j = (n : ℤ) • P.root j := by simpa
    rw [(smul_left_injective ℤ <| P.ne_zero j).eq_iff, eq_comm] at hj
    have : 2 ≤ n := Nat.AtLeastTwo.prop
    lia
  · rw [← one_smul ℤ (P.root i), ← neg_smul, hj] at this
    replace this : (n : ℤ) • P.root i = -1 • P.root i := by simpa
    rw [(smul_left_injective ℤ <| P.ne_zero i).eq_iff] at this
    lia

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

Goal state before:
pp: case refine_1
ι : 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✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : 2 • P.root j ∈ range ⇑P.root
hij : i = j
⊢ False

Tactic:
exact P.nsmul_notMem_range_root h

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
P : RootPairing ι R M N
inst✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
⊢ ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)

Tactic:
rintro i - ⟨j, rfl⟩

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✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
i j : ι
⊢ (preReflection (coroot i) (p (root i))) (coroot j) ∈ range ⇑coroot
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
⊢ j ∈ Finset.univ → (Q j) (Pi.single i x j) = 0

Tactic:
_

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
⊢ (Q j) (Pi.single i x j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ∧ (pi Q).Anisotropic ↔
    ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic

Tactic:
nonneg_pi_iff

Goal state after:
ι : Type u_1
R : Type u_2
Mᵢ : ι → Type u_8
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → Module R (Mᵢ i)
P : Type u_10
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid P
inst✝² : PartialOrder P
inst✝¹ : IsOrderedAddMonoid P
inst✝ : Module R P
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (pi Q).Anisotropic ↔ ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ (Q i) x) ∧ (Q i).Anisotropic
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
⊢ polar (⇑(pi Q)) x y = ∑ i, polar (⇑(Q i)) (x i) (y i)

Tactic:
dsimp [polar]
  simp_rw [Finset.sum_sub_distrib, pi_apply, Pi.add_apply]

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
i : ι
hi : i ∈ {x ∈ s | c x < 0}
j : ι
hj : j ∈ {i ∈ s | 0 < c i}
⊢ 0 ≤ c i * (c j * (B (v j)) (v i))

Tactic:
grind [Pairwise, mul_nonneg_iff, mul_nonpos_iff]

Goal state after:
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
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
cases subsingleton_or_nontrivial L
  · exact IsEmpty.elim inferInstance α
  simpa [chainTopCoeff_zero_right α hα] using
    genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
⊢ (((ofMulAction k G H) g) f).coeff h = f.coeff (g⁻¹ • h)

Tactic:
by
  conv_lhs => rw [← smul_inv_smul g h]
  set h' := g⁻¹ • h
  have hg : Function.Injective (g • · : H → H) := by
    intro h₁ h₂
    simp
  simp [ofMulAction_def, Finsupp.mapDomain_apply, hg]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x y : k[G]
⊢ ((ofMulAction k G G).asAlgebraHom x) y = x * y

Tactic:
induction x using induction_on with
  | of g => ext; simp [MonoidAlgebra.coeff_single_mul_apply]
  | add x y hx hy => simp [hx, hy, add_mul]
  | smul r x hx => simp [← hx]

Goal state after:
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
⊢ B.rootLength i ≤ B.rootLength j

Tactic:
by
  have h : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
      ({(1, 1), (1, 2), (1, 3), (1, 4), (-1, -1), (-1, -2), (-1, -3), (-1, -4)} : Set (ℤ × ℤ)) := by
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
  simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at h
  have h' := B.pairingIn_mul_eq_pairingIn_mul_swap i j
  have hi := B.rootLength_pos i
  rcases h with hij' | hij' | hij' | hij' | hij' | hij' | hij' | hij' <;>
  rw [hij'.1, hij'.2] at h' <;> lia

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

Goal state before:
pp: case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ : M
⊢ ∀ (y : M),
    x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      y ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
        (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
          (∃ f, Function.support f ⊆ ↑b.support ∧ y = ∑ j ∈ b.support, f j • P.root j) →
            ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y = ∑ j ∈ b.support, f j • P.root j

Tactic:
_

Goal state after:
case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
⊢ x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
    y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
        (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
          ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
⊢ x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
    y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
        (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
          ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j

Tactic:
_

Goal state after:
case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
    (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
      (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
        ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
    (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
      (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
        ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j

Tactic:
_

Goal state after:
case refine_2
ι : 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
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hy✝ : y✝ ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ (∃ f, Function.support f ⊆ ↑b.support ∧ x✝ = ∑ j ∈ b.support, f j • P.root j) →
    (∃ f, Function.support f ⊆ ↑b.support ∧ y✝ = ∑ j ∈ b.support, f j • P.root j) →
      ∃ f, Function.support f ⊆ ↑b.support ∧ x✝ + y✝ = ∑ j ∈ b.support, f j • P.root j
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 k : ι
hk : P.root k = P.root j + P.root i
h : LinearIndependent R ![P.root i, P.root k]
⊢ chainTopCoeff i j = chainTopCoeff i k + 1

Tactic:
replace hk : P.root j = P.root k - P.root i := by rw [hk]; abel

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 k : ι
h : LinearIndependent R ![P.root i, P.root k]
hk : P.root j = P.root k - P.root i
⊢ chainTopCoeff i j = chainTopCoeff i k + 1
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 (chainBotIdx i j) = P.root j - chainBotCoeff i j • P.root i

Tactic:
by_cases h : LinearIndependent R ![P.root i, P.root j]
  · simp only [chainBotIdx, reduceDIte, h]
    exact (P.root_sub_nsmul_mem_range_iff_le_chainBotCoeff h).mpr
      (le_refl <| P.chainBotCoeff i j) |>.choose_spec
  · simp only [chainBotIdx, chainBotCoeff, h, reduceDIte, zero_smul, sub_zero]

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

Goal state before:
pp: A : Type u_5
inst✝³ : CommRing A
inst✝² : IsDomain A
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι A
⊢ (toBilin' M).Nondegenerate ↔ M.det ≠ 0

Tactic:
by
  rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ { cauchy := a + -b } = { cauchy := a } - { cauchy := b }

Tactic:
ofCauchy_add,

Goal state after:
a b : Cauchy abs
⊢ { cauchy := a } + { cauchy := -b } = { cauchy := a } - { cauchy := b }
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
⊢ ε✝ > 0 → ∃ i, ∀ j ≥ i, |↑(a ⊔ b - b) j| < ε✝

Tactic:
_

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a ⊔ b - b) j| < ε✝
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ u ⬝ᵥ w ≤ v ⬝ᵥ w

Tactic:
unfold dotProduct; gcongr <;> apply_rules

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Fintype n
u v w : n → R
huv : u ≤ v
hw : 0 ≤ w
⊢ w ⬝ᵥ u ≤ w ⬝ᵥ v

Tactic:
unfold dotProduct; gcongr <;> apply_rules

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
⊢ ε✝ > 0 → ∃ i, ∀ j ≥ i, |↑(a ⊓ b - b) j| < ε✝

Tactic:
_

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a ⊓ b - b) j| < ε✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr.succ
b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑(b + 1) + 1 ≤ (a + 1) ^ (b + 1)

Tactic:
| succ b hb =>

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ f 1 ^ 2 = f 1

Tactic:
conv_rhs => rw [← one_pow 2, hf _ one_le_two]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ ∑ i, A i.2 i.1 * B i.2 i.1 = ∑ i, ∑ j, Aᵀ i j * B j i

Tactic:
transpose_apply,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ ∑ i, A i.2 i.1 * B i.2 i.1 = ∑ i, ∑ j, A j i * B j i
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, B k x.1 * A l x.2 * X.vec x = ∑ x, ∑ i, A l i * X i x * Bᵀ x k

Tactic:
transpose_apply,

Goal state after:
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, B k x.1 * A l x.2 * X.vec x = ∑ x, ∑ i, A l i * X i x * B k x
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, X.vec x * (B x.1 k * A x.2 l) = ∑ x, ∑ i, Aᵀ l i * X i x * B x k

Tactic:
transpose_apply,

Goal state after:
l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, X.vec x * (B x.1 k * A x.2 l) = ∑ x, ∑ i, A i l * X i x * B x k