mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : 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
⊢ 0 ≤ ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ↔ x ≤ y

pp: case pos
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
⊢ ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ≤ 0 ↔ x ≤ y

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✝³ : 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
⊢ ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ≤
      ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ↔
    x ≤ y

Tactic:
· simp [hx0]

Goal state after:
case pos
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
⊢ ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ≤ 0 ↔ x ≤ y

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✝³ : 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
⊢ ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ≤
      ↑(valueGroup.mk (ofClass w) (↑⋯.choose).1 (↑⋯.choose).2 ⋯ ⋯) ↔
    x ≤ y
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
S : Type u_6
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i j k l : ι
h : P.root k = P.root i + P.root l
⊢ P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j

Tactic:
by
  apply FaithfulSMul.algebraMap_injective S R
  simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using pairing_eq_add_of_root_eq_add h

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ finrank K ↥(Q.rootSpan K) = finrank L M

Tactic:
LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ finrank L M = finrank L M

case hM
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ span L ↑(Q.rootSpan K) = ⊤

case hN
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ span L ↑(Q.corootSpan K) = ⊤

case hp
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ ∀ x ∈ Q.rootSpan K, ∀ y ∈ Q.corootSpan K, (Q.toLinearMap x) y ∈ (algebraMap K L).range
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ finrank K ↥(Q.rootSpan K) = finrank L M

Tactic:
rw [LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)]
  · simp
  · simp
  · exact Q.toLinearMap_apply_apply_mem_range_algebraMap K

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✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : ↥(P.rootSpan S)
⊢ (P.PolarizationIn S) x = ∑ i, (P.coroot'In S i) x • P.coroot i

Tactic:
by
  simp [PolarizationIn]

Goal state after:
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✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.rootSpan S)

Tactic:
← finrank_range_polarization_eq_finrank_span_coroot

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
⊢ finrank S ↥(P.PolarizationIn S).range ≤ finrank S ↥(P.rootSpan S)
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✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsTorsionFree S M
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(Submodule.map (P.PolarizationIn S) ⊤)

Tactic:
← finrank_range_polarization_eq_finrank_span_coroot

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsTorsionFree S M
⊢ finrank S ↥(P.PolarizationIn S).range ≤ finrank S ↥(Submodule.map (P.PolarizationIn S) ⊤)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: 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✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : v.supp = ⊤
⊢ v 1 = 0

Tactic:
by rw [← mem_supp_iff, h]; exact Submodule.mem_top

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ⇑(span R (Set.range b)).subtype '' ↑(span R (Set.range fun i ↦ ⟨b i, ⋯⟩))

Tactic:
rwa [← map_coe, ← span_image, ← Set.range_comp]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
key : ↑s.card < sxy.encard
⊢ ∃ z₁ z₂, z₁ ≠ z₂ ∧ f z₁ = f z₂

Tactic:
obtain ⟨z₁, -, z₂, -, h⟩ := exists_ne_map_eq_of_encard_lt_of_maps_to (by simpa) hf'

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
key : ↑s.card < sxy.encard
z₁ z₂ : ↑sxy
h : z₁ ≠ z₂ ∧ f z₁ = f z₂
⊢ ∃ z₁ z₂, z₁ ≠ z₂ ∧ f z₁ = f z₂
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: case h
ι : 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
hc : ∑ i ∈ s, c i • v i = 0
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
⊢ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s

Tactic:
grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_filter]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

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
g : G
x : RestrictScalars k k[G] ρ.asModule
⊢ ((ofModule ρ.asModule) g) x =
    (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k k[G] ρ.asModule) x))))

Tactic:
dsimp [ofModule, RestrictScalars.lsmul_apply_apply]

Goal state after:
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
g : G
x : RestrictScalars k k[G] ρ.asModule
⊢ (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (MonoidAlgebra.single g 1 • (RestrictScalars.addEquiv k k[G] ρ.asModule) x) =
    (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k k[G] ρ.asModule) x))))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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
e : (reflectRoot α β).IsZero
hα : α.IsZero
⊢ β (coroot α) = 0

Tactic:
simp [coroot_eq_zero_iff.mpr hα]

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
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht : t • P.root i ∈ range ⇑P.root
⊢ t = 1 ∨ t = -1

Tactic:
by
  obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht
  replace ht : (z : R) • P.coroot i ∈ range P.coroot := by
    obtain ⟨j, hj⟩ := ht
    simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hz, one_smul] using mem_range_self j
  obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h _ ht
  have : (z : R) * w = 1 := by
    simpa [mul_mul_mul_comm _ t, mul_comm t, mul_comm _ (z : R), hz] using congr_arg₂ (· * ·) hz hw
  suffices z = 1 ∨ z = -1 by
    rcases this with rfl | rfl
    · left; simpa using hz
    · right; simpa [neg_eq_iff_eq_neg] using hz
  norm_cast at this
  rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this
  tauto

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 j]
⊢ chainBotCoeff i j = sSup {k | P.root j - k • P.root i ∈ range ⇑P.root}

Tactic:
rw [← Iic_chainBotCoeff_eq h, csSup_Iic]

Goal state after:
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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
⊢ Nat.card ↑(baseOf (⇑P.root) f) = finrank R M

Tactic:
let b : Basis (baseOf P.root f) ℚ (P.rootSpan ℚ) := by
      replace this : LinearIndependent ℚ v :=
        .of_comp (P.rootSpan ℚ).subtype <| P.linearIndepOn_root_baseOf' f.toRatLinearMap hf
      exact Basis.mk this (by rw [h_span])

Goal state after:
ι : 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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_span : span ℚ (range v) = ⊤
b : Basis ↑(baseOf (⇑P.root) f) ℚ ↥(P.rootSpan ℚ) :=
  have this := ⋯;
  Basis.mk this ⋯
⊢ Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
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 : ι
⊢ chainBotCoeff i ((P.reflectionPerm j) j) = chainTopCoeff i j

Tactic:
let := P.indexNeg
  have (z : ℤ) : z ∈ Icc (-P.chainTopCoeff i j : ℤ) (P.chainBotCoeff i j) ↔
      z ∈ Icc (-P.chainBotCoeff i (-j) : ℤ) (P.chainTopCoeff i (-j)) := by
    rw [P.chainCoeff_reflectionPerm_right_aux]
  refine le_antisymm ?_ ?_
  · simpa using this (-P.chainBotCoeff i (-j))
  · simpa using this (-P.chainTopCoeff i j)

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
⊢ ⊤ ≤ span ℤ (range fun i ↦ P.rootSpanMem ℤ ↑i)

Tactic:
have : (fun i : b.support ↦ P.rootSpanMem ℤ i) = P.rootSpanMem ℤ ∘ ((↑) : b.support → ι) := rfl
    simp [this, range_comp]

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
⊢ b.height k = ∑ j ∈ b.support, f j + ∑ j ∈ b.support, g j

Tactic:
height_eq_sum hfg,

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 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 = ∑ j ∈ b.support, f j + ∑ j ∈ b.support, g j
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
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : P.root i = u • ∑ x, a x • ↑x + v • ∑ x, b x • ↑x
⊢ u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1

Tactic:
Finset.smul_sum,

Goal state after:
ι : 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
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : P.root i = ∑ x, u • a x • ↑x + ∑ x, v • b x • ↑x
⊢ u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
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 : ι
z : ℤ
hk : P.root k = P.root i + z • 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 + z • g) l • P.root l
⊢ b.height k = ∑ j ∈ b.support, f j + z • ∑ j ∈ b.support, g j

Tactic:
height_eq_sum hfg,

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 j k : ι
z : ℤ
hk : P.root k = P.root i + z • 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 + z • g) l • P.root l
⊢ ∑ j ∈ b.support, (f + z • g) j = ∑ j ∈ b.support, f j + z • ∑ j ∈ b.support, g j
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case step
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i✝ : ℕ
h : ∀ j ≥ i✝, abv (f j - f i✝) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
j : ℕ
hj : j.le i
⊢ abv (f j) ≤ R i.succ

Tactic:
exact (hi j hj).trans (le_max_left _ _)

Goal state after: