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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id * LinearMap.id + LinearMap.id * ↑n • LinearMap.smulRight (f - g) x +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x * ↑n • LinearMap.smulRight (f - g) x) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x

Tactic:
simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
        add_assoc, Nat.cast_succ, add_smul, one_smul]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
val✝ : Fintype m
A' : Matrix m m ↥K := of fun i j ↦ ⟨A.submatrix id (⇑e) i j, ⋯⟩
hA' : A'.map ⇑K.subtype = A.submatrix id ⇑e
hA : IsUnit A'
B' : Matrix m m ↥K
hB : A' * B' = 1
this : (B'.submatrix (⇑e.symm) id).map ⇑K.subtype = B
⊢ B i j ∈ K

Tactic:
by simp [← this]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ↑(den A r) ∣ p.leadingCoeff * num A r ^ p.natDegree

Tactic:
rw [← coeff_scaleRoots_natDegree]

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ↑(den A r) ∣ (p.scaleRoots ?s).coeff p.natDegree * num A r ^ p.natDegree

case s
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ A
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℤ
⊢ T R (m * n) = (T R m).comp (T R n)

Tactic:
induction m using Polynomial.Chebyshev.induct with

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℤ
⊢ C R (m * n) = (C R m).comp (C R n)

Tactic:
induction m using Polynomial.Chebyshev.induct with

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊤

Tactic:
← s_last

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥(RelSeries.last s)
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
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleModule R M

Tactic:
isSimpleModule_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleOrder (Submodule R M)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2

Tactic:
refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
⊢ a ∣ b ∨ b ∣ a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x) → v x ≤ min 1 γ

pp: case mpr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ v x ≤ min 1 γ → ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
· rintro ⟨y, hy, rfl⟩
    rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩
    · rw [h]
      exact y.prop
    · rw [h]
      exact hy

Goal state after:
case mpr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ v x ≤ min 1 γ → ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
h : ↑x n = 0
⊢ ↑x m ∈ I ^ n • ⊤

Tactic:
simpa [mapQ, h, ← LinearMap.mem_ker, ker_liftQ] using x.prop m_ge

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

Goal state before:
pp: case h.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
r : R
hr : r ∈ I
⊢ r ∈ span {p ^ Nat.find ex}

Tactic:
by_cases hr0 : r = 0

Goal state after:
case pos
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
r : R
hr : r ∈ I
hr0 : r = 0
⊢ r ∈ span {p ^ Nat.find ex}

case neg
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
r : R
hr : r ∈ I
hr0 : ¬r = 0
⊢ r ∈ span {p ^ Nat.find ex}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
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
n : ℕ
u : Rˣ
hr : p ^ n * ↑u ∈ I
hr0 : ¬p ^ n * ↑u = 0
⊢ p ^ Nat.find ex ∣ p ^ n

Tactic:
apply pow_dvd_pow

Goal state after:
case neg
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
n : ℕ
u : Rˣ
hr : p ^ n * ↑u ∈ I
hr0 : ¬p ^ n * ↑u = 0
⊢ Nat.find ex ≤ n
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ (under R (Ideal.map (algebraMap R S) I)).IsMaximal ∧ y ∉ under R (Ideal.map (algebraMap R S) I)

Tactic:
under_map_of_isPrime_disjoint (powers y) S hI.isPrime

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ I.IsMaximal ∧ y ∉ I

R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ Disjoint ↑(powers y) ↑I
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: 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
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ ∃ b, (1 + -x * y) * b = 1

Tactic:
use L

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : ↑v * ϖ ^ m ∈ nonZeroDivisors R
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) ≠ 0
⊢ ∃ n_1 u_1, (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) = u_1 • (algebraMap R K) ϖ ^ n_1

Tactic:
have hϖ' : algebraMap R K ϖ ≠ 0 := by simpa using hϖ.ne_zero

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : ↑v * ϖ ^ m ∈ nonZeroDivisors R
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) ≠ 0
hϖ' : (algebraMap R K) ϖ ≠ 0
⊢ ∃ n_1 u_1, (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) = u_1 • (algebraMap R K) ϖ ^ n_1
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ∀ b ∈ {J | I ≤ J ∧ J.IsPrime}, IsLocalRing.maximalIdeal R ≤ b

Tactic:
· rintro J ⟨h₁, h₂⟩
    exact (Ring.KrullDimLE.eq_maximalIdeal_of_isPrime J).ge

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : Associates R
⊢ x ∈ (Associates R)⁰ ↔ ↑((associatesEquivIsPrincipal R) x) ∈ (Ideal R)⁰

Tactic:
by rw [← quot_out x, mk_mem_nonZeroDivisors_associates,
          associatesEquivIsPrincipal_apply, span_singleton_nonZeroDivisors]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective
    ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I) ∘ₗ ↑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)))

Tactic:
LinearEquiv.coe_rTensor,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I) ∘ₗ rTensor M ↑(Ideal.isoBaseOfIsPrincipal h))
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : IsTorsionFree R M
⊢ Flat R M

Tactic:
rw [IsDedekindDomain.flat_iff_torsion_eq_bot, ← Submodule.isTorsionFree_iff_torsion_eq_bot]
  infer_instance

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
this✝¹ : IsReflexive R N
this✝ : IsTorsionFree S N
i : ι
x✝ : i ∈ Finset.univ
h : ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) = 0
this : (algebraMap S R) (((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) = 0
⊢ False

Tactic:
rw [algebraMap_rootFormIn] at this

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 N
this✝ : IsTorsionFree S N
i : ι
x✝ : i ∈ Finset.univ
h : ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) = 0
this : (P.RootForm ↑(P.rootSpanMem S i)) ↑(P.rootSpanMem S i) = 0
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i j : ι
hj : P.root j = n • P.root i
this : n • P.root i = -1 • P.root i
⊢ False

Tactic:
replace this : (n : ℤ) • P.root i = -1 • P.root i := by simpa

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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i j : ι
hj : P.root j = n • P.root i
this : ↑n • P.root i = -1 • P.root i
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case h
ι : 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 : ι
⊢ root ((RootPairing.equiv_of_mapsTo p root coroot i hs hp) j) = (preReflection (root i) (p.flip (coroot i))) (root j)

Tactic:
rw [equiv_of_mapsTo_apply, (exist_eq_reflection_of_mapsTo p root coroot i j hs).choose_spec]

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))
z : ↑sxy
x✝ : z ∈ univ
⊢ f z ∈ ↑s

Tactic:
by specialize hf z; aesop

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

Goal state before:
pp: case neg.a
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 (⇑α) β ≤ chainLength α β

Tactic:
← Nat.le_sub_iff_add_le (chainTopCoeff_le_chainLength α β),

Goal state after:
case neg.a
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 (⇑α) β ≤ chainLength α β - chainTopCoeff (⇑α) β
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.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 : α
i : G
b : k
⊢ MonoidAlgebra.single g a • Finsupp.single h (MonoidAlgebra.single i b) =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h (MonoidAlgebra.single i b))

Tactic:
| single i b =>

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
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : P.coxeterWeightIn ℤ i j ≤ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
simp only [hcn, mem_insert_iff, mem_singleton_iff] at 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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : ↑n ≤ 4
⊢ ↑n = 0 ∨ ↑n = 1 ∨ ↑n = 2 ∨ ↑n = 3 ∨ ↑n = 4
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : 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 = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ range ⇑P.root

Tactic:
have : P.chainBotCoeff i j = 0 ↔ Iic (P.chainBotCoeff i j) = {0} := by
    simpa [Set.ext_iff, mem_Iic, mem_singleton_iff] using ⟨fun h ↦ by simp [h], fun h ↦ by rw [← h]⟩

Goal state after:
case pos
ι : 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]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
⊢ chainBotCoeff i j = 0 ↔ ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j - P.root i ∉ range ⇑P.root
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ { cauchy := ⟦f⟧ }.lt { cauchy := ⟦g⟧ } ↔ f < g

Tactic:
lt_def

Goal state after:
f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 ↦ x1 < x2) definition._proof_1✝) ↔
    f < g
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ 0⁻¹ = 0

Tactic:
by simp [← ofCauchy_zero, ← ofCauchy_inv]

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_notMem : μ ∉ Set.range d
this : Disjoint (eigenspace ((toLin b b) (diagonal d)) μ) ⊤
⊢ False

Tactic:
disjoint_top

Goal state after:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_notMem : μ ∉ Set.range d
this : eigenspace ((toLin b b) (diagonal d)) μ = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (↑m * ↑n) = A ^ ↑(m * n)

Tactic:
Int.natCast_mul

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (↑m * ↑n) = A ^ (↑m * ↑n)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i

Tactic:
simpa using h.2 (x := .single i 1)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix n m R
hA : A.PosDef
hB : Function.Injective B.mulVec
⊢ (Bᴴ * A * B).PosDef

Tactic:
by
  refine of_dotProduct_mulVec_pos (isHermitian_conjTranspose_mul_mul _ hA.1) fun x hx => ?_
  have : B *ᵥ x ≠ 0 := fun h => hx <| hB.eq_iff' (mulVec_zero _) |>.1 h
  simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.dotProduct_mulVec_pos this

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

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

Tactic:
Nat.cast_mul,

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
⊢ InjOn ⇑(LinearMap.fst R L₁ L₂) ↑(span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})

Tactic:
by
  suffices ∀ y, (∃ l : ι₁ →₀ R,
      (l.linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) = (0, y)) → y = 0 by
    have aux : {(b₁.h i, b₂.h (eι i)) | i : ι₁} = (fun i : ι₁ ↦ (b₁.h i, b₂.h (eι i))) '' univ := by
      ext; simp
    simp_rw [← LinearMap.disjoint_ker_iff_injOn, LinearMap.disjoint_ker, aux,
      mem_span_image_iff_linearCombination]
    aesop
  intro y ⟨f, hf⟩
  suffices linearCombination R b₁.h f = 0 by
    rw [LinearMap.map_eq_zero_iff _ b₁.linInd] at this
    aesop (add simp Prod.ext_iff)
  replace hf := (LinearMap.fst R L₁ L₂).congr_arg hf
  rw [← LinearMap.comp_apply, ← Finsupp.linearCombination_linear_comp] at hf
  aesop

Goal state after: