mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace H 0) (U ⊔ V)
⊢ V ⊔ ⨆ i ∈ s0, LieModule.genWeightSpace L i =
    (⨆ x ∈ sV, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ s0, LieModule.genWeightSpace L x

Tactic:
hsV'

Goal state after:
case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace H 0) (U ⊔ V)
⊢ (⨆ i ∈ sV, LieModule.genWeightSpace L i) ⊔ ⨆ i ∈ s0, LieModule.genWeightSpace L i =
    (⨆ x ∈ sV, LieModule.genWeightSpace L x) ⊔ ⨆ x ∈ s0, LieModule.genWeightSpace L x
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case e'_5
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
h₀ : Disjoint (rootSpace H 0) (U ⊔ V)
h₁ : Disjoint U (V ⊔ rootSpace H 0)
⊢ rootSpace H 0 ⊔ U = ⨆ i ∈ s0 ∪ sU, LieModule.genWeightSpace L i

Tactic:
rw [iSup_union, hs0', hsU']

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  ↑(∏ l ∈ Finset.range k, (2 * l + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))
⊢ ↑(∏ l ∈ Finset.range (k + 1), (2 * l + 1)) * eval 1 ((⇑derivative)^[k + 1] (T R n)) =
    ↑(∏ l ∈ Finset.range (k + 1), (n ^ 2 - ↑l ^ 2))

Tactic:
push_cast at ih ⊢

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih : (∏ x ∈ Finset.range k, (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k] (T R n)) = ∏ x ∈ Finset.range k, (↑n ^ 2 - ↑x ^ 2)
⊢ (∏ x ∈ Finset.range (k + 1), (2 * ↑x + 1)) * eval 1 ((⇑derivative)^[k + 1] (T R n)) =
    ∏ x ∈ Finset.range (k + 1), (↑n ^ 2 - ↑x ^ 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  ↑(∏ l ∈ Finset.range k, (2 * l + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)
⊢ ↑(∏ l ∈ Finset.range (k + 1), (2 * l + 3)) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    ↑(∏ l ∈ Finset.range (k + 1), ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)

Tactic:
push_cast at ih ⊢

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
ih :
  (∏ x ∈ Finset.range k, (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    (∏ x ∈ Finset.range k, ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
⊢ (∏ x ∈ Finset.range (k + 1), (2 * ↑x + 3)) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1), ((↑n + 1) ^ 2 - (↑x + 1) ^ 2)) * (↑n + 1)
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsUnit ↑(den A 0)

Tactic:
simp [isUnit_den_iff, IsLocalization.isInteger_zero]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
exact h (Nat.le_succ n)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥

Tactic:
refine eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ sInf (map C '' {J | J.IsMaximal}) ≤ ⊥
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
hϖ' : (algebraMap R K) ϖ ≠ 0
⊢ (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) = (u / v) • (algebraMap R K) ϖ ^ (↑n - ↑m)

Tactic:
simp [hϖ', zpow_sub₀, div_smul_div_comm, Units.smul_def u, Units.smul_def v, Algebra.smul_def]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < 1
⊢ v (1 - x) = 1

Tactic:
rw [← v.map_one, ← v.map_neg] at h
  rw [sub_eq_add_neg 1 x]
  simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

Tactic:
obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n * ↑u ∈ I
hs₂ : x ^ n * ↑u ∉ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case right
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀✝
v✝ : Valuation R Γ₀✝
Γ₀ : Type u_7
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : v x ≠ 0
h1 : v x ≠ 1
⊢ Units.mk0 (v x) h0 ≠ 1

Tactic:
simpa [Units.ext_iff]

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
r : R
hr : r ∈ R⁰
inst✝ : Flat R M
⊢ IsSMulRegular M r

Tactic:
apply isSMulRegular_of_isRegular
  exact le_nonZeroDivisors_iff_isRegular.mp (le_refl R⁰) ⟨r, hr⟩

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) ∘ₗ ↑(Ideal.isoBaseOfIsPrincipal h)))

Tactic:
LinearMap.comp_assoc,

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 ∘ₗ ↑(Ideal.isoBaseOfIsPrincipal h)))
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 ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ ∃ c, ∑ i, c i • P.coroot i = ∑ i, (P.coroot' i) ↑x • P.coroot i

Tactic:
use fun i => P.toLinearMap x (P.coroot i)

Goal state after:
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✝ : Fintype ι
y : N
x : ↥(P.rootSpan R)
hx : (P.Polarization.domRestrict (P.rootSpan R)) x = y
⊢ ∑ i, (fun i ↦ (P.toLinearMap ↑x) (P.coroot i)) i • P.coroot i = ∑ i, (P.coroot' i) ↑x • P.coroot i
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x y : R
w✝¹ : (ofClass v) x ≠ 0
w✝ : (ofClass v) y ≠ 0
⊢ h.orderMonoidIso ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝) =
    (OrderMonoidIso.refl (ofClass v).ValueGroup₀) ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝)

Tactic:
· simp [orderMonoidIso, valueGroup₀Fun_spec h]

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

Tactic:
have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h

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 : (algebraMap S R) (((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) = 0
⊢ False
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp
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✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₁ : Q₁.Anisotropic
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic

Tactic:
exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩

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✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Tactic:
by
  simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
  constructor
  · rintro ⟨⟨hle₁, hle₂⟩, ha⟩
    obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
    exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
  · rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
    refine ⟨⟨hle₁, hle₂⟩, ?_⟩
    rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
    rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
    rwa [Prod.mk_eq_zero]

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

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✝ : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
⊢ pred 1 ⋯

Tactic:
obtain ⟨i⟩ : Nonempty ι := inferInstance

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✝ : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
i : ι
⊢ pred 1 ⋯
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]
  simp

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

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
p q : ↥ρ.invtSubmodule
h :
  {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p ≤
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      q
x : V
hx : x ∈ ↑p
⊢ ρ.asModuleEquiv.symm x ∈
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p

Tactic:
by simpa using hx

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

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ ⟨q, hq⟩ = ⊥ ∨ ⟨q, hq⟩ = ⊤

Tactic:
simp only [invtRootSubmodule.bot_mem, invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff,
      Subtype.mk_eq_top_iff]

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ q = ⊥ ∨ q = ⊤
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
this : ∀ (z : α), x < z → y ≤ z
z : α
⊢ z ∈ Ioo x y ↔ z ∈ ∅

Tactic:
simpa using this z

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 : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p

Tactic:
have h_ne : S.Nonempty := ⟨0, by simp [S_def]⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j ≤ 0

Tactic:
rw [← sub_le_sub_iff_right, zero_sub]

Goal state after:
case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ ↑f j - ?inr.refine_2✝ ≤ -?inr.refine_2✝

case inr.refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : ↑f i ≤ 0
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ -↑f i
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ α
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk y✝¹ ⊔ mk y✝

Tactic:
rw [← mk_sup, mk_le]

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝¹ ≤ y✝¹ ⊔ y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk y✝¹ ⊔ mk y✝

Tactic:
rw [← mk_sup, mk_le]

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝ ≤ y✝¹ ⊔ y✝
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 g : CauSeq β abv
⊢ f.lim + (-g).lim = (f + -g).lim

Tactic:
lim_add f (-g)

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 g : CauSeq β abv
⊢ (f + -g).lim = (f + -g).lim
Module: Mathlib.LinearAlgebra.Matrix.ZPow

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

Tactic:
rw [det_pow]

Goal state after:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X ^ n.succ).det

Tactic:
rw [det_pow]

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X.det ^ n.succ)
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y ^ n.succ).det

Tactic:
rw [det_pow]

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y.det ^ n.succ)