mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ↑(length R (M ⧸ N)) = ↑(Order.coheight N)

Tactic:
Order.coheight_eq_krullDim_Ici,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ ↑(length R (M ⧸ N)) = Order.krullDim ↑(Set.Ici N)
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
N : Submodule R M
⊢ Order.height N < ⊤

Tactic:
simpa only [← Module.length_submodule] using Module.length_ne_top.lt_top

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

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : c⁻¹ • e • (fun m ↦ m • b) d = c⁻¹ • (fun m ↦ m • a) c
⊢ (↑c⁻¹ * e * ↑d) • b = a

Tactic:
simpa [mul_smul] using! he

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a c : R
⊢ ∃ c_1, f a * c_1 = f (a * c) ∨ f (a * c) * c_1 = f a

pp: case inr
R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
b c : R
⊢ ∃ c_1, f (b * c) * c_1 = f b ∨ f b * c_1 = f (b * c)

Tactic:
exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
⊢ span {p ^ Nat.find ex} ≤ I

Tactic:
· rw [span_singleton_le_iff_mem]
    exact Nat.find_spec ex

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ n, Associated x (ϖ ^ n)

Tactic:
by
  have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
  obtain ⟨fx, hfx⟩ := WfDvdMonoid.exists_factors x hx
  use Multiset.card fx
  have H := hfx.2
  rw [← Associates.mk_eq_mk_iff_associated] at H ⊢
  rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
  congr 1
  rw [Multiset.eq_replicate]
  simp only [true_and, and_imp, Multiset.card_map, Multiset.mem_map, exists_imp]
  rintro _ _ _ rfl
  rw [Associates.mk_eq_mk_iff_associated]
  refine associated_of_irreducible _ ?_ hirr
  apply hfx.1
  assumption

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

Goal state before:
pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ (1 - x * y) * f (n✝ + 1) - 1 ∈ I ^ (n✝ + 1)

Tactic:
← neg_sub _ (1 : R),

Goal state after:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ -(x * y - 1) * f (n✝ + 1) - 1 ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
x✝ : Ideal R
⊢ x✝ ∈ minimalPrimes R ↔ x✝ ∈ {I | I.IsMaximal}

Tactic:
simp [minimalPrimes_eq_setOfPred_isPrime, Ideal.isMaximal_iff_isPrime]

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

Goal state before:
pp: case hB
ι : 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
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ ∀ x ∈ range ⇑P.root,
    ∀ y ∈ range ⇑P.root, ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) x) y ∈ (Algebra.linearMap S R).range

pp: case hx
ι : 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
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ (span S (range ⇑P.root)).subtype ⟨x, hx⟩ ∈ span S (range ⇑P.root)

pp: case hy
ι : 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
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ (span S (range ⇑P.root)).subtype ⟨y, hy⟩ ∈ span S (range ⇑P.root)

Tactic:
· rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
      simpa using B.exists_eq i j

Goal state after:
case hx
ι : 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
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ (span S (range ⇑P.root)).subtype ⟨x, hx⟩ ∈ span S (range ⇑P.root)

case hy
ι : 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
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ (span S (range ⇑P.root)).subtype ⟨y, hy⟩ ∈ span S (range ⇑P.root)
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
⊢ P.rootSpan R = ⊤ ↔ P.corootSpan R = ⊤

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> apply Submodule.eq_top_of_finrank_eq
  · rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
  · rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq,
      Subspace.dual_finrank_eq]

Goal state after:
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
S : Type u_5
i j : ι
inst✝⁷ : Finite ι
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R M
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ P.pairingIn S i j = -2 ∧ P.pairingIn S j i = -2 ↔ P.root i = -P.root j

Tactic:
simp only [← P.pairing_neg_two_neg_two_iff, ← P.algebraMap_pairingIn S,
    ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff, ← map_neg]

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

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x

Tactic:
simp_rw [Prod.forall, prod_apply]

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ polar (⇑(Q₁.prod Q₂)) x y = polar (⇑Q₁) x.1 y.1 + polar (⇑Q₂) x.2 y.2

Tactic:
by
  dsimp [polar]
  abel

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
t : k
g : G
v : ρ.asModule
⊢ MonoidAlgebra.single g t • v = (t • ρ g) (ρ.asModuleEquiv v)

Tactic:
← asAlgebraHom_single,

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
t : k
g : G
v : ρ.asModule
⊢ MonoidAlgebra.single g t • v = (ρ.asAlgebraHom (MonoidAlgebra.single g t)) (ρ.asModuleEquiv v)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inl
ι : 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
w : ℤ
hz : ↑1 * t = 1
ht : ↑1 • P.coroot i ∈ range ⇑P.coroot
hw : ↑w * ↑1 = 1
this : ↑1 * ↑w = 1
⊢ t = 1 ∨ t = -1

pp: case inr
ι : 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
w : ℤ
hz : ↑(-1) * t = 1
ht : ↑(-1) • P.coroot i ∈ range ⇑P.coroot
hw : ↑w * ↑(-1) = 1
this : ↑(-1) * ↑w = 1
⊢ t = 1 ∨ t = -1

Tactic:
· left; simpa using hz

Goal state after:
case inr
ι : 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
w : ℤ
hz : ↑(-1) * t = 1
ht : ↑(-1) • P.coroot i ∈ range ⇑P.coroot
hw : ↑w * ↑(-1) = 1
this : ↑(-1) * ↑w = 1
⊢ t = 1 ∨ t = -1
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)
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)

Tactic:
let v (i : baseOf P.root f) : P.rootSpan ℚ := P.rootSpanMem ℚ i

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
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr
ι : 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 : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
classical
  let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
  have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_neg]
  intro contra
  rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
  · simpa [hij, f] using le_of_lt pos j
  · simpa [hij, f] using le_of_lt neg i

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

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
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : P.IsCrystallographic
inst✝³ : IsDomain R
inst✝² : P.IsReduced
B : P.InvariantForm
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
i j : ι
hji_ne : (B.form (P.root j)) (P.root j) ≠ (B.form (P.root i)) (P.root i)
k : ι
hki_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root i)) (P.root i)
hkj_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root j)) (P.root j)
⊢ False

Tactic:
have hij := (B.apply_eq_or i j).resolve_left hji_ne.symm

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
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : P.IsCrystallographic
inst✝³ : IsDomain R
inst✝² : P.IsReduced
B : P.InvariantForm
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
i j : ι
hji_ne : (B.form (P.root j)) (P.root j) ≠ (B.form (P.root i)) (P.root i)
k : ι
hki_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root i)) (P.root i)
hkj_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root j)) (P.root j)
hij :
  (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨
    (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨
      (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)
⊢ False
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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
x✝ : ℤ
⊢ x✝ ∈ {z | P.root j + z • P.root i ∈ range ⇑P.root} ↔ x✝ ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

Tactic:
mem_ofPred_eq,

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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
x✝ : ℤ
⊢ P.root j + x✝ • P.root i ∈ range ⇑P.root ↔ x✝ ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i 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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
x✝ : ℤ
⊢ x✝ ∈ {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root} ↔
    x✝ ∈ Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))

Tactic:
mem_ofPred_eq,

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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
x✝ : ℤ
⊢ P.root (chainTopIdx i j) + x✝ • P.root i ∈ range ⇑P.root ↔
    x✝ ∈ Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ (∑ i ∈ b.support, ⇑(f i • P.toLinearMap (P.root i))) (P.coroot i) =
    ∑ x ∈ b.support, f x • (algebraMap ℤ R) (P.pairingIn ℤ x i)

Tactic:
Finset.sum_apply,

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
inst✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ ∑ c ∈ b.support, (f c • P.toLinearMap (P.root c)) (P.coroot i) =
    ∑ x ∈ b.support, f x • (algebraMap ℤ R) (P.pairingIn ℤ x i)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ { cauchy := ↑(n + 1) }.cauchy = ({ cauchy := ↑n } + 1).cauchy

Tactic:
simp [cauchy_one, cauchy_add]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
⊢ f.lim = 0

Tactic:
have h₁ : f = f - const abv 0 := ext fun n => by simp

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K - K / 2 ≤ ↑(y✝ - f) j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j

Tactic:
sub_self_div_two,

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
j : ℕ
ij : j ≥ i
this : K / 2 ≤ ↑(y✝ - f) j + (↑f j - ↑f i)
⊢ K / 2 ≤ ↑(y✝ - const abs (↑f i)) j
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ A ⊙ 1 = diagonal d ↔ A.diag = d

Tactic:
by
  simpa using hadamard_diagonal_eq_diagonal_iff (A := A) (d := 1)

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

Goal state before:
pp: ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst✝ : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x✝ : n × m
⊢ (∑ i ∈ s, A i) x✝.2 x✝.1 = (∑ i ∈ s, (A i).vec) x✝

Tactic:
Finset.sum_apply,

Goal state after:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst✝ : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x✝ : n × m
⊢ (∑ i ∈ s, A i) x✝.2 x✝.1 = ∑ c ∈ s, (A c).vec x✝
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
f : n ≃ m
⊢ ((reindex f f) A).IsHermitian ↔ A.IsHermitian

Tactic:
by
  refine ⟨fun h ↦ ?_, (·.reindex f)⟩
  simpa using h.reindex f.symm

Goal state after: